StepFourSigmaBar

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

Step 4's σ-arithmetic at the anchor's index pair (m, j−2)

What Step 4 needs, and what is proved here

Step 4 of the proof of l.bounds.mathcal.E.aL (ff.) reads Step 3's display at the index pair (m, j−2) -- the recentering scale m against the 𝒢₂-cutoff scale j−2 of the cube □_j. Three scalar inputs of that reading are σ-arithmetic and are proved here:

• (B1) σ_m^{-1} σ_{j−2} ≤ 4 -- the ratio slot, at every pair j − 2 ≤ m;
• (B3) 3^{γ j} σ_{j−2}^{-1} ≤ 4 c⋆^{-1/2} γ^{1/2} -- the gauge slot, i.e. the lower branch of the e.shom.h.bounds rearranged, with the index shift 3^{2γ} ≤ 2 already paid;
• (B2) the square of l.shom.continuity's fifth conclusion at the shifted pair, which is the shape in which (σ_m σ_{j−2}^{-1} − 1)^2 occurs in Step 3's display, with the shift factor 3^{4γ} ≤ 2 absorbed into the constant.

(B1) and (B3) are stated in the printed regime only: their induction-state binder is discharged internally by GoodEvents.exists_allScalesInductionState (the manuscript's own discharge), so nothing is left for a caller beyond γ ≤ C^{-10} c⋆^{10}.

(B2) cannot be made binder-free: l.shom.continuity carries the landmark gate m** < m₀, the induction state at m₀ − 1 and the two E-window gates, and its right-hand side mentions E. Those binders are carried honestly below. The E-free corollary ..._gammaAbsorbed replaces E² γ |log γ|² by γ^{3/5} |log γ|² using only the printed regime γ ≤ E^{-10} and 1 ≤ E (through the proved E ≤ γ^{-1/5} window), so a consumer that does not want to carry E in the display still keeps the two structural binders.

Constants

Every constant below is explicit: 4 in (B1), 4 c⋆^{-1/2} in (B3), and max C (2C²) in (B2), where C is l.shom.continuity's own constant. The max is what lets one constant serve both as the budget gate C c⋆^{-1} ≤ E and as the display constant.

References

• ABK26, l.bounds.mathcal.E.aL, ff. (Step 4); l.shom.continuity, (its fifth conclusion ff.); e.shom.h.bounds; p.induction.bounds proof.

B1: the ratio slot

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

(B1) The σ ratio at the anchor's index pair.

σ_m^{-1} σ_{j−2} ≤ 4 for every pair with j − 2 ≤ m, in the printed regime alone: the induction-state binder of Annular.SigmaBarBudget.sigmaBar_ratio_le_four is discharged by the all-scales state, at m₀ := m.

B3: the gauge slot

theorem Algsuperdiff.Section4.Provider.BoundsEaL.exists_rpow_gamma_mul_inv_sigmaBar_sub_two_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 - 2)))⁻¹ ≤ 4 * ((√(Section3.Disorder.cstar M))⁻¹ * √M.gamma)

(B3) The gauge slot.

3^{γ j} σ_{j−2}^{-1} ≤ 4 c⋆^{-1/2} γ^{1/2}: the lower branch of the e.shom.h.bounds, read at the shifted index j − 2 (where the proved Annular.SigmaBarBudget.inv_sigmaBar_sub_two_le_of_inductionState has already paid the index shift 3^{2γ} ≤ 2, at the honest constant 4), multiplied by the gauge weight 3^{γ j}.

The γ^{1/2} on the right is what Step 4's moment pass converts into the anchor's √γ; the c⋆^{-1/2} is the subsection's constant convention.

B2: the squared continuity display at the shifted pair

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

(B2) The squared continuity display at the shifted pair.

l.shom.continuity's fifth conclusion at (n, m) := (j−2, m), squared:

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

The second summand of the printed left-hand side (|σ_{j−2} σ_m^{-1} − 1|) is dropped by nonnegativity; the index shift is paid by 3^{4γ} ≤ 2, absorbed into the constant.

B2 with E absorbed into a power of γ

theorem Algsuperdiff.Section4.Provider.BoundsEaL.exists_sigmaBar_ratio_sub_one_sq_le_gammaAbsorbed (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d) (m0 : ℤ) (E : { E : ℝ // 1 ≤ E }), Section3.mStarStar M < m0 → Frozen.Section3.inductionState M (m0 - 1) E → C * (Section3.Disorder.cstar M)⁻¹ ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → M.gamma ≤ 1 / 8 → ∀ (m j : ℤ), j - 2 ≤ m → m ≤ m0 → (↑(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), E-free. The squared continuity display at the shifted pair with the budget E absorbed: E² γ |log γ|² ≤ γ^{3/5} |log γ|².

The two structural binders (the landmark gate and the induction state) remain, because l.shom.continuity genuinely needs them; only the E occurring in the display is removed.