SigmaBarIndex

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

The σ index conversion at a two-scale gap, binder-free

This module closes that conversion inside the anchor's own regime: the induction-state binder that Annular.SigmaBarBudget.sigmaBar_ratio_le_four carries is discharged internally by GoodEvents.exists_allScalesInductionState, at the landmark m₀ := n+2 (resp. m₀ := n), so nothing beyond γ ≤ C^{-1} c⋆^{10} is asked of the caller. This is the B1 wrapper pattern of Provider/BoundsEaL/StepFourSigmaBar.lean, re-derived here so that the BoundsEaL tree is not imported.

   σ_{n+2}^{-1} ≤ 4 σ_n^{-1}        (the direction the anchor's display needs)
   σ_n^{-1}     ≤ 7 σ_{n+2}^{-1}    (the converse, at the same regime)

Both constants are absolute numerals: no s, no γ, no c⋆, no dimension. The regime is written in the frozen theorem's own shape γ ≤ C^{-1} c⋆^{10} (the induction-state producer's shape γ ≤ (C₀^{-1})^{10} c⋆^{10} is reached by exporting C := C₀^{10}).

Where the constants come from

σ is almost monotone in the scale, in both directions, because the induction state pins σ_m^2 inside a factor-4 window around max(c⋆ γ^{-1} 3^{2γm}, ν^2), and that window's own ratio across two scales is 3^{4γ} ≤ 3 at the standing γ ≤ 1/4. Upward: the window is monotone in m, so the two factor-4 branches give σ_n ≤ 4 σ_{n+2}. Downward: the extra 3^{4γ} ≤ 3 gives σ_{n+2}^2 ≤ 48 σ_n^2, i.e. σ_{n+2} ≤ 7 σ_n.

References

• ABK26, e.shom.h.bounds; p.induction.bounds proof.

1. Two arithmetic helpers

2. The two ratio readings of the state

theorem Algsuperdiff.Section4.Provider.ExcessDecay.inv_sigmaBar_add_two_le_of_inductionState {d : ℕ} (M : Section3.ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) {n : ℤ} (hn : n + 2 ≤ m0) : (↑(Section3.Annealed.sigmaBar M (n + 2)))⁻¹ ≤ 4 * (↑(Section3.Annealed.sigmaBar M n))⁻¹

σ is almost increasing. From the induction state at the landmark n+2: σ_n ≤ 4 σ_{n+2}, in the inverse form the force leg consumes.

3. The binder-free exports

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

The σ index conversion the anchor's force leg needs, binder-free.

In the frozen theorem's own regime alone, σ_{n+2}^{-1} ≤ 4 σ_n^{-1} at every integer scale: the induction-state binder is discharged internally.