ShomContinuityUngated

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

The σ-continuity difference in the shape §4.1 consumes it

ABK26, the display e.shom.m.vs.shom.n (the conclusion of l.shom.continuity) and its §4.1 consumption inside p.mathcalE.annular.decomp, Step 3:

  sum_{n <= m} 3^{-s(m-n)} |σ_m σ_{n-2}^{-1} - 1|^2
    <= C sum_{n <= m} 3^{-s(m-n)}
         min{ γ(m-n) + c⋆^{-2} γ |log γ|^2 , 1 }^2 3^{2γ(m-n)} .

The per-n inequality behind that first step is the hshom slot of Provider.Annular.ClauseOne.clauseOne_bound, and this module supplies it without the Section 3 gate list.

The four gates, and how each is discharged

The proved Section 3 statement Algsuperdiff.Section3.Provider.Localization.shom_continuity delivers, as its fifth conjunct, the symmetrized display

  |σ_m σ_n^{-1} - 1| + |σ_n σ_m^{-1} - 1|
      <= C min{1, γ(m-n) + E^2 γ |log γ|^2} 3^{γ(m-n)}

for n <= m <= m₀, behind four gates: the landmark m** < m₀, the induction state 𝒮(m₀-1,E), the budget C c⋆^{-1} <= E, and the regime γ <= E^{-10}. Here:

• the landmark and the scale gate are free. m₀ occurs in the statement only through m <= m₀ and m** < m₀, and the conclusion does not mention m₀ at all; so for the pair (m,n) at hand one takes m₀ := max m (m** + 1) (exists_landmark_scale). No case split at the landmark, and no below-landmark σ fact, is needed: the choice is available for every m, including m <= m**.
• Its C₀-floor is what lets the budget constant of l.shom.continuity be requested by name.
• the budget gate C_shc c⋆^{-1} <= E is mul_cstarInv_le_of_budget at the floor C₀ := C_shc.
• the regime γ <= E^{-10} is returned with the state at the budget identity E = C c⋆^{-1}; the surviving hypothesis is the printed γ <= C^{-10} c⋆^{10}, which is the regime p.induction.bounds is stated under.

E^2 versus c⋆^{-2}, and the index orientation

The manuscript's Step-3 display is the Section 3 display "at E ≍ c⋆^{-1}". That is a two-sided reading of the budget, and only the lower half (E >= C c⋆^{-1}) is a hypothesis of l.shom.continuity; the upper half is available here because the state is produced at the identity E = C c⋆^{-1}, so E^2 = C^2 (c⋆^2)^{-1} exactly. Since min{1, x + K z} <= K min{1, x + z} for K >= 1 and x,z >= 0 (min_one_add_mul_le), the printed c⋆^{-2}-bracket follows at the cost of one further constant factor, and the min is preserved rather than discarded.

The Section 3 conjunct is symmetric in the two ratio defects, so no orientation is lost: with n <= m it bounds |σ_m σ_n^{-1} - 1| and |σ_n σ_m^{-1} - 1| simultaneously. §4.1 needs the first, at the shifted lower index n-2 (the σ_{n-2} of the per-cube ugly estimate); n <= m-1 gives n-2 <= m, and γ(m-(n-2)) = γ(m-n) + 2γ is exactly the +2γ printed inside the slot's bracket. The leftover 3^{2γ} from the same shift is absorbed into the constant using γ <= 1.

What is delivered

• exists_sigmaBar_defect_ge — the symmetrized display at every pair n <= m, under the printed regime alone, with the min intact and the bracket in c⋆^{-2} form.
• exists_shomSlot_ge — the squared, index-shifted, min-free form that is literally the hshom slot of clauseOne_bound.

References

• ABK26, l.shom.continuity / e.shom.m.vs.shom.n; the §4.1 consumption.
• p.induction.bounds, (the terminal budget).

1. Abstract-real arithmetic

Five one-purpose facts on opaque reals: no Real.rpow, log or exp atom is ever exposed to a numeric tactic here.

2. The landmark gate

theorem Algsuperdiff.Section4.Provider.Annular.exists_landmark_scale {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) : ∃ (m0 : ℤ), Section3.mStarStar M < m0 ∧ m ≤ m0

The landmark and the scale gate cost nothing.

l.shom.continuity quantifies over an auxiliary top scale m₀ subject to m** < m₀ and m ≤ m₀, and its conclusion does not mention m₀. Both constraints are met at once by m₀ := max m (m** + 1), for every m — in particular below the landmark, where no separate base-plateau σ fact is needed.

3. The de-gated defect display

theorem Algsuperdiff.Section4.Provider.Annular.exists_sigmaBar_defect_ge (d : ℕ) (C₀ : ℝ) : ∃ (C : ℝ), 6 ≤ C ∧ C₀ ≤ C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → ∀ (m n : ℤ), n ≤ m → |↑(Section3.Annealed.sigmaBar M m) * (↑(Section3.Annealed.sigmaBar M n))⁻¹ - 1| + |↑(Section3.Annealed.sigmaBar M n) * (↑(Section3.Annealed.sigmaBar M m))⁻¹ - 1| ≤ C * min 1 (M.gamma * (↑m - ↑n) + (Section3.Disorder.cstar M ^ 2)⁻¹ * (M.gamma * |Real.log M.gamma| ^ 2)) * 3 ^ (M.gamma * (↑m - ↑n))

e.shom.m.vs.shom.n, de-gated, with a caller-prescribed constant floor.

For every requested threshold C₀ there is a C ≥ max 6 C₀, depending only on the dimension and on C₀, such that every model in the printed regime γ ≤ C^{-10} c⋆^{10} satisfies, at every pair of integer scales n ≤ m,

  |σ_m σ_n^{-1} - 1| + |σ_n σ_m^{-1} - 1|
      ≤ C min{1, γ(m-n) + c⋆^{-2} γ|log γ|^2} 3^{γ(m-n)} .

No landmark, no scale gate, no induction-state premise, no budget parameter: the bracket is the manuscript's Step-3 bracket, i.e. the printed E^2 read at E ≍ c⋆^{-1}, which is legitimate because the state is produced at the budget identity.

4. The hshom slot

theorem Algsuperdiff.Section4.Provider.Annular.exists_shomSlot_ge (d : ℕ) (C₀ : ℝ) : ∃ (Cshom : ℝ), 6 ≤ Cshom ∧ C₀ ≤ Cshom ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ Cshom⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → ∀ (m n : ℤ), n ≤ m - 1 → (↑(Section3.Annealed.sigmaBar M m) * (↑(Section3.Annealed.sigmaBar M (n - 2)))⁻¹ - 1) ^ 2 ≤ (Cshom * M.gamma * ↑(m - n) + Cshom * (2 * M.gamma + (Section3.Disorder.cstar M ^ 2)⁻¹ * (M.gamma * |Real.log M.gamma| ^ 2))) ^ 2 * 3 ^ (2 * M.gamma * ↑(m - n))

The hshom slot of clauseOne_bound, unconditional in the printed regime, with a caller-prescribed constant floor.

For every requested threshold C₀ there is a Cshom ≥ max 6 C₀, depending only on the dimension and on C₀, such that every model with γ ≤ Cshom^{-10} c⋆^{10} satisfies, for all integer scales n ≤ m - 1,

  |σ_m σ_{n-2}^{-1} - 1|^2
    ≤ ( Cshom γ (m-n) + Cshom (2γ + c⋆^{-2} γ|log γ|^2) )^2 3^{2γ(m-n)} .

The 2γ inside the bracket and the constant factor 9 inside Cshom are the two halves of the index shift n ↦ n-2: γ(m-(n-2)) = γ(m-n) + 2γ in the bracket, and 3^{2γ} ≤ 9 in the growth factor.