High-contrast homogenization: Entry.Multiscale.Initial.EntryGeneration

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

Initialization: Steps 3 and 4, the entry generation and the geometry there

Step 3 (p.initial.fixed.grid.scale): the per-step decrement and the determinant budget force a generation n₀ in [R, R + ⌈C log₃(2+Π)⌉] at which 𝒫_Id(n₀;j_*) + D_{Id,j_*}(n₀) ≤ η₀, and the carried history majorization converts that into the bound on ℋ_Id(n₀) + D_{Id,j_*}(n₀). Step 4 of p.initial.fixed.grid.scale supplies the deterministic geometry at that generation from the entry-radius estimate.

theorem HCPolySupport.HighContrast.Multiscale.exists_entry_generation_eta0 (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ η₀ ∈ Set.Ioc 0 1, ∃ (C : ℝ), 0 < C ∧ ∀ (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 → ∀ (R : ℤ), ↑jStar ≤ R → ∃ (n₀ : ℤ), R ≤ n₀ ∧ n₀ ≤ R + ⌈C * Real.logb 3 (2 + aspectRatio E)⌉ ∧ profile P γ 1 jStar (↑jStar) n₀ + determinantDrift P γ 1 jStar n₀ ≤ η₀

E7 (kernel). Step 3, the hitting index: some n₀ = T_ℓ, ℓ < K, has 𝒫_Id(n₀;j_*) + D_{Id,j_*}(n₀) ≤ η₀, and R ≤ n₀ ≤ R + ⌈C log₃(2+Π)⌉.

theorem HCPolySupport.HighContrast.Multiscale.exists_entry_generation (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ ηinit ∈ Set.Ioc 0 1, ∃ (C : ℝ), 0 < C ∧ ∀ (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 → ∀ (R : ℤ), ↑jStar ≤ R → ∃ (n₀ : ℤ), R ≤ n₀ ∧ n₀ ≤ R + ⌈C * Real.logb 3 (2 + aspectRatio E)⌉ ∧ profile P γ 1 jStar n₀ n₀ + determinantDrift P γ 1 jStar n₀ ≤ ηinit

E8. e.renormalization.entry (p.initial.fixed.grid.scale): the smallness at n₀ in the form 𝒫_Id(n₀;n₀) + D_{Id,j_*}(n₀) ≤ η_init, via carried majorization and η₀ := η_init / max 1 C.

F. Step 4 — geometry (p.initial.fixed.grid.scale)

theorem HCPolySupport.HighContrast.Multiscale.geometry_at_generation (d : ℕ) (hd : 2 ≤ d) : ∃ (Cgeom : ℝ), 0 < Cgeom ∧ ∀ γ ∈ Set.Ico 0 1, ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ (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 → ∀ (n₀ : ℤ), ↑jStar ≤ n₀ → 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)

F1. e.initial.geometry.bounds at every generation n₀ ≥ j_*: the two-sided block comparison and the entry radius; Cgeom depends on d alone and is chosen before γ.