High-contrast homogenization: Entry.Multiscale.Global.RunStepAny

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

The Selects projections the run needs and the per-step case analysis

This module serves the scale-selection proposition p.scale.selection. The run quantifies over a selection datum S : SelectionData with S.Selects d γ, and the module extracts from Selects the three inequalities the run needs: selects_two_bigQ_le_h (2 * bigQ d γ ≤ S.h, the generation gap consumed by Entry.fixed_geometry_one_grid_propagation_full), selects_one_le_L (1 ≤ S.L ε σ, the scale gap needed by long_step_decrease.hL), and the bridge sandwich at δ = √ε σ, L = S.L ε σ under the run's source threshold. It then proves run_step_any, the five-way case analysis of Selects at a run state, which derives the containment hcont and step hstep binders of run_exists_stop; the remaining assembly is in HCPoly.Entry.Multiscale.Global.RunAssembly.

§1 The three facts the run needs, carried by Selects

theorem HCPolySupport.HighContrast.Multiscale.selects_two_bigQ_le_h (d : ℕ) (_hd : 2 ≤ d) (γ : ℝ) (_hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (hS : S.Selects d γ) : 2 * bigQ d γ ≤ S.h

C1 of SelectionData.Selects (near p.scale.selection, s.polynomial.entry.proof): the generation gap is at least 2Q, so Entry.fixed_geometry_one_grid_propagation_full applies at the step length.

theorem HCPolySupport.HighContrast.Multiscale.selects_one_le_L (d : ℕ) (_hd : 2 ≤ d) (γ : ℝ) (_hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (hS : S.Selects d γ) (ε σ : ℝ) (hε : ε ∈ Set.Ioc 0 S.eps0) (hσ : σ ∈ Set.Ioc 0 ε) : 1 ≤ S.L ε σ

C2a of SelectionData.Selects (p.scale.selection, e.bridge.length.choice): the scale gap is a length, as long_step_decrease.hL needs.

§2 The per-step case analysis

theorem HCPolySupport.HighContrast.Multiscale.run_step_any {d : ℕ} (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (hS : S.Selects d γ) (hh : 2 * bigQ d γ ≤ S.h) (hL : ∀ (ε σ : ℝ), ε ∈ Set.Ioc 0 S.eps0 → σ ∈ Set.Ioc 0 ε → 1 ≤ S.L ε σ) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∃ (Cbase : ℝ), 0 < Cbase ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (ε σ B : ℝ), ε ∈ Set.Ioc 0 S.eps0 → σ ∈ Set.Ioc 0 ε → S.B0 ε σ ≤ B → ∀ (H jStar : ℕ), max 4 S.h ≤ H → 2 * d ≤ 3 ^ jStar → (∀ (C' : ℝ), 0 < C' → C' ≤ Csrc → ⌈C' * Real.logb 3 (2 * K)⌉ ≤ ↑jStar) → ∀ (n₀ : ℤ), ↑jStar + ⌈B * Real.logb 3 (2 + aspectRatio E)⌉ ≤ n₀ → ∀ (Cinit : ℝ), 0 ≤ Cinit → n₀ ≤ ↑jStar + ⌈B * Real.logb 3 (2 + aspectRatio E)⌉ + ⌈Cinit * Real.logb 3 (2 + aspectRatio E)⌉ → ∀ (a c C w : ℝ), 1 ≤ C → ↑d ≤ C → Cbase ≤ C → 1 ≤ a → ↑d ≤ a → w = a * C / ↑d → c = 1 / 2 * S.eta ε σ * Real.log (16 / 9) → 4 * ↑(bigQ d γ) * max 1 C ≤ a * C / ↑d → Real.log (1 + C * ↑S.h) + c ≤ a * ε / 2 → 4 * (Real.log (1 + 2 * C * ↑(S.L ε σ)) + Real.log (1 + C * ↑H) + c) ≤ a * C * ε * σ → 0 ≤ Real.log (1 + C * ↑H) → 1 / 2 * Real.log ((1 + √ε * σ) / (1 - √ε * σ)) + 2 * C * (↑S.h + 2) * Real.log (1 + √ε * σ) ≤ min (ε / 2) (C * σ / 4) → ∀ (J : ℕ), (∀ j ≤ n₀ + (2 * ↑(S.L ε σ) + ↑H + ↑S.h) * (↑J + 2), ↑j + (Real.logb 3 (2 * √(4 * ↑d)) + ε * (↑J + 1) / Real.log 3) ≤ 2 * ↑jStar) → (∀ (st : RunState P γ S ε σ B E H jStar n₀), st.i ≤ J → adaptedCell (Geometry.explicitRoundedGrid jStar st.m) (st.n + 2 * ↑(S.L ε σ)) ∪ adaptedCell (Geometry.explicitRoundedGrid jStar (geometryUpdate ε st.m (explicitCanonicalMetric (adaptedMean P ⋯ ⋯)))) (st.n + ↑(S.L ε σ)) ⊆ centeredCube d (2 * ↑jStar)) ∧ ∀ (st : RunState P γ S ε σ B E H jStar n₀), st.i ≤ J → (∃ (st' : RunState P γ S ε σ B E H jStar n₀), st'.i = st.i + 1 ∧ runGauge P γ jStar (S.eta ε σ) a w S.h st'.m st'.k st'.n - runGauge P γ jStar (S.eta ε σ) a w S.h st.m st.k st.n ≤ -c) ∨ RunStopData P γ S ε σ B E H jStar n₀ Cbase st

The five-way case analysis of Selects at a run state — the hcont and hstep binders of run_exists_stop, as one theorem.

Route. Fix a state st with st.i ≤ J.

• Containment (hcont): run_entry_containment at m := st.m, mP := 𝔪₊, j := st.n + 2L, jP := st.n + L, e := ε * (J + 1); the two eccentricity premises come from st.hecc (and, for 𝔪₊, from st.hpr through Geometry.projectiveDistance_geometryUpdate_le), and hj/hjP are hcontA, the containment_arith instance at its free real argument d := 4d, fed by st.hgen.
• Step (hstep): apply hS at st.m, st.k, st.n, with entry premises the source threshold at the Selects source constant, st.hecc, st.hone, st.hgap and the containment just built; then case-split on the five disjuncts: Alt-1 start-up is vacuous by st.hlt, Alt-1 service is run_step_service, Alt-2 with 𝔪₊ ≠ 𝔪⋆ is run_step_change, Alt-2 with 𝔪₊ = 𝔪⋆ is run_step_failed_test when the determinant test fails and the RIGHT disjunct (the stop) when it succeeds, Alt-3 synchronized is run_step_sync and Alt-3 long is run_step_long. The propagation clauses hprop1/hspan of run_step_sync/run_step_failed_test/run_step_long come from Entry.fixed_geometry_one_grid_propagation_full under hh, and the bridge sandwiches hbr₁/hbr₂ of run_step_change/run_step_failed_test from Selects' conjunct C3; both source thresholds are discharged by hsrc.

Csrc is existential because the Selects, propagation and bridge source constants are Skolem constants of their own statements: the theorem chooses their maximum.

The existential ∃ Cbase and the binder Cbase ≤ C are present because the Selects transport constant and the one-grid propagation constant must both sit below the run's C; neither follows from 1 ≤ C, (d : ℝ) ≤ C. The scales_arith and eccentricity_arith hypotheses are not assumed: they are unused by this conclusion, contradictory with the comparison_choice binder at the same C, and needed only by run_stop_output at the output constant. The stop disjunct is RunStopData … Cbase, which carries the Alternative-2 bridge sandwich and output bound.