SigmaBarLandmark

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Step 5's landmark: the continuity binders discharged, and the σ index shift

What this module does

Three bookkeeping items that Step 5 of l.bounds.mathcal.E.aL needs before its Hölder assembly can be written down.

1. Bullet (B2) without the continuity binders. Bullet (B2) of Step 4 (StepFourSigmaBar.exists_sigmaBar_ratio_sub_one_sq_le) carries l.shom.continuity's own binders: the landmark gate m** < m₀, the induction state at m₀ − 1, and the two E-window gates, whereas §4.5 quotes the continuity lemma hypothesis-free. They are removable at Step 5's own landmark: m₀ := max m (m** + 1) satisfies BOTH m ≤ m₀ and m** < m₀ unconditionally, and GoodEvents.exists_allScalesInductionState_ge supplies the induction state at every scale together with the budget identity E = C c⋆^{-1} and the regime γ ≤ E^{-10}. The result is (B2) in the printed regime alone (plus γ ≤ 1/8, which Step 3's display already carries), with the E-free display of the _gammaAbsorbed corollary.

2. The σ index reconciliation. The (B5) bullet is delivered at the gauge σ_{j−1} while Step 3's display and the remaining Step-4 bullets are read at σ_{j−2}. The two are interchangeable at the constant 4, binder-free in the printed regime, by the same hratio slot that produces (B1).

3. The dimension binder-order. A statement of the shape ∃ C, 0 < C ∧ ∀ M : ABKModel d, … may be proved under 2 ≤ d and then stated without it, because an ABKModel d carries 2 ≤ d itself; the d < 2 branch is vacuous. This is the exact move the anchor's own binder order (∃ C before ∀ M) requires.

References

• ABK26, l.bounds.mathcal.E.aL, Step 4 bullets (B1)/(B2)/(B5); l.shom.continuity; e.shom.h.bounds.

1. The dimension binder order

theorem Algsuperdiff.Section4.Provider.BoundsEaL.exists_pos_forall_model_of_two_le_dimension {d : ℕ} {Q : ℝ → Section3.ABKModel d → Prop} (h : 2 ≤ d → ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), Q C M) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), Q C M

The 2 ≤ d binder, removed from the statement.

This is the move that lets a provider match the anchor's binder order, where ∃ C precedes ∀ M.

2. The σ index reconciliation σ_{j−1} ↔ σ_{j−2}

theorem Algsuperdiff.Section4.Provider.BoundsEaL.exists_inv_sigmaBar_sub_one_le_four_mul_inv_sigmaBar_sub_two (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → ∀ (j : ℤ), (↑(Section3.Annealed.sigmaBar M (j - 1)))⁻¹ ≤ 4 * (↑(Section3.Annealed.sigmaBar M (j - 2)))⁻¹

The (B5) gauge, moved to the (B1)/(B2)/(B3) index.

σ_{j−1}^{-1} ≤ 4 σ_{j−2}^{-1} for every j, in the printed regime alone: Annular.SigmaBarBudget.sigmaBar_ratio_le_four at the index pair (m, n) := (j−1, j), whose induction-state binder is discharged internally at the landmark m₀ := j − 1 by the all-scales state.

This is the conversion Step 5 needs in order to read LambdaSlotConsumer's (B5) majorant (stated at σ_{R.scale−1}) against (B3)'s gauge slot (stated at σ_{R.scale−2}).

theorem Algsuperdiff.Section4.Provider.BoundsEaL.gamma_regime_mono {C C' cst gam : ℝ} (hC : 0 < C) (hCC : C ≤ C') (hcst : 0 ≤ cst) (h : gam ≤ C'⁻¹ ^ 10 * cst ^ 10) : gam ≤ C⁻¹ ^ 10 * cst ^ 10

The printed regime is monotone in the constant. Enlarging C in γ ≤ C^{-10} c⋆^{10} strengthens the hypothesis, so a bullet proved at C is available at any larger constant. This is what lets one constant serve a composition of several proved bullets.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.exists_rpow_gamma_mul_inv_sigmaBar_sub_one_le (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → ∀ (j : ℤ), 3 ^ (M.gamma * ↑j) * (↑(Section3.Annealed.sigmaBar M (j - 1)))⁻¹ ≤ 16 * ((√(Section3.Disorder.cstar M))⁻¹ * √M.gamma)

(B3) at the (B5) index.

3^{γ j} σ_{j−1}^{-1} ≤ 16 c⋆^{-1/2} γ^{1/2}: the gauge slot of Step 4, read at the index j − 1 that bullet (B5) delivers, through the index reconciliation σ_{j−1}^{-1} ≤ 4 σ_{j−2}^{-1}. The constant 16 is the printed 4 of (B3) times the reconciliation's 4.

This is the factor that makes Step 5's bracket O(√γ): it is the ONLY place where the product ‖∇(k_L−k_{j−2})‖ · λ^{-1} of the two Step-4 bullets is converted into a γ-power.

3. Bullet (B2) without the continuity binders

theorem Algsuperdiff.Section4.Provider.BoundsEaL.exists_sigmaBar_ratio_sub_one_sq_le_unconditional (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → M.gamma ≤ 1 / 8 → ∀ (m j : ℤ), j - 2 ≤ m → (↑(Section3.Annealed.sigmaBar M m) * (↑(Section3.Annealed.sigmaBar M (j - 2)))⁻¹ - 1) ^ 2 ≤ C * min 1 (M.gamma * (↑m - ↑j + 2) + M.gamma ^ (3 / 5) * |Real.log M.gamma| ^ 2) ^ 2 * 3 ^ (2 * (M.gamma * (↑m - ↑j)))

(B2), unconditional in the printed regime.

The squared l.shom.continuity display at the anchor's index pair, with ALL of the continuity lemma's binders discharged:

(σ_m σ_{j−2}^{-1} − 1)²
    ≤ C (min{1, γ(m−j+2) + γ^{3/5}|log γ|²})² 3^{2γ(m−j)} ,      j − 2 ≤ m .

The landmark is Step 5's own: m₀ := max m (m** + 1) meets the gate m** < m₀ and the range binder m ≤ m₀ at once, and the induction state at m₀ − 1 (with the budget identity E = C c⋆^{-1} and the regime γ ≤ E^{-10}) is GoodEvents.exists_allScalesInductionState_ge, i.e. the manuscript's own discharge.

The only binder beyond the printed regime is γ ≤ 1/8, which Step 3's display already carries.