High-contrast homogenization: Entry.InitialFixedGridScale

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Initialization fixed-grid-scale

The type repeats the initialization statement HCPoly/Entry/Statements/InitialFixedGridScale.lean (p.initial.fixed.grid.scale): same binders, same binder kinds and order, same six conjuncts, the source-lower-scale premise where the statement has it, and no additional hypothesis. The two unused ∀ binders carry a leading underscore: _hγ, _hS.

The proof combines the entry generation from Step 3 and the geometry from Step 4. It chooses Cgeom before γ and S, Csrc after S and before ηinit, and C after ηinit and before the remaining data.

theorem HCPolySupport.HighContrast.Entry.initial_fixed_grid_scale (d : ℕ) (hd : 2 ≤ d) : ∃ (Cgeom : ℝ), 0 < Cgeom ∧ ∀ γ ∈ Set.Ico 0 1, ∀ (S : SelectionData), S.Selects d γ → ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ ηinit ∈ Set.Ioc 0 1, ∃ (C : ℝ), 0 < C ∧ ∀ (ε σ : ℝ), 0 < σ → σ ≤ ε → ε ≤ S.eps0 → ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (B : ℝ), S.B0 ε σ ≤ B → ∃ (n₀ : ℤ), ↑jStar + ⌈B * Real.logb 3 (2 + aspectRatio E)⌉ ≤ n₀ ∧ n₀ ≤ ↑jStar + ⌈B * Real.logb 3 (2 + aspectRatio E)⌉ + ⌈C * Real.logb 3 (2 + aspectRatio E)⌉ ∧ profile P γ 1 jStar n₀ n₀ + determinantDrift P γ 1 jStar n₀ ≤ ηinit ∧ BlockMatLoewnerLE (blockScale (1 / 2) (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d)))) (adaptedMean P 1 n₀) ∧ BlockMatLoewnerLE (adaptedMean P 1 n₀) (blockScale 2 E) ∧ projectiveDistance 1 (explicitCanonicalMetric (adaptedMean P 1 n₀)) ≤ Cgeom * Real.log (2 + 4 * aspectRatio E)

Proof of p.initial.fixed.grid.scale. Repeats the statement of HCPolySupport.HighContrast.initial_fixed_grid_scale (HCPoly/Entry/Statements/InitialFixedGridScale.lean, p.initial.fixed.grid.scale) byte for byte up to the underscore-prefixed unused binders _hγ, _hS: same binder kinds and order, Cgeom before γ and S, Csrc after S and before η_init, C after η_init and before ε, σ, the law, j_* and B, the source-scale premise, and the six conjuncts in the printed order.