SigmaBarBudget

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

The σ slots of Step 2, at the honest 𝒢₁ amplitude

ABK26, Section 4.1, p.mathcalE.annular.decomp Step 2. UglyLatticeChain.exists_uglyJEstimate_lattice_cube carries five σ-shaped inputs:

• hkap0, hkap — the normalization γ κ² = c⋆;
• hsigmlow — ½ κ 3^{γm} ≤ σ_m;
• hsignlow — ¼ κ 3^{γn} ≤ σ_{n−2} (the relaxed constant);
• hratio — σ_m^{−1} σ_{n−2} ≤ C_r;

together with the gauge input hshell. This module discharges all of them from the Section 3 induction state and from ShellGaugeBudget, at the honest clause-(i) amplitude

T' = √c⋆ γ^{−1/2}    (so  T' = κ  exactly).

The hsignlow constant, stated honestly

The frozen Frozen.Section3.inductionState gives σ_k² ≥ ¼ max(c⋆ γ^{−1} 3^{2γk}, ν²), hence at k = n − 2

σ_{n−2} ≥ ½ κ 3^{γ(n−2)} = 3^{−2γ} · ( ½ κ 3^{γn} ) ,

which is short of the printed ½ κ 3^{γn} by exactly the factor 3^{2γ} (≤ 3^{1/16} ≈ 1.072 on the printed window 8γ ≤ s ≤ 1/4). The ugly chain's hsignlow binder was relaxed to ¼ for exactly this reason, and SignLowDischarge discharges it outright from sigmaBar_lower_of_inductionState below. inv_sigmaBar_sub_two_le_of_inductionState is the inverse form of the same fact, and it is what the hshell producer here consumes.

Part A -- the amplitude is the chain's κ

theorem Algsuperdiff.Section4.Provider.Annular.annularEventAmplitude_pos {d : ℕ} (M : Section3.ABKModel d) : 0 < √(Section3.Disorder.cstar M) * (√M.gamma)⁻¹

The honest clause-(i) 𝒢₁ amplitude T' = √c⋆ γ^{−1/2} is positive.

theorem Algsuperdiff.Section4.Provider.Annular.gamma_mul_annularEventAmplitude_sq {d : ℕ} (M : Section3.ABKModel d) : M.gamma * (√(Section3.Disorder.cstar M) * (√M.gamma)⁻¹) ^ 2 = Section3.Disorder.cstar M

The chain's hkap slot at the honest amplitude: γ T'² = c⋆. The 𝒢₁ threshold of the printed clause-(i) event is the κ of e.ugly.estimate.for.J; no rescaling intervenes.

Part B -- the σ readings of the induction state

theorem Algsuperdiff.Section4.Provider.Annular.sigmaBar_lower_of_inductionState {d : ℕ} (M : Section3.ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) {k : ℤ} (hk : k ≤ m0) : 1 / 2 * (√(Section3.Disorder.cstar M) * (√M.gamma)⁻¹ * 3 ^ (M.gamma * ↑k)) ≤ ↑(Section3.Annealed.sigmaBar M k)

The hsigmlow slot. The lower branch of e.shom.h.bounds, at the honest amplitude, at any scale below the landmark.

theorem Algsuperdiff.Section4.Provider.Annular.inv_sigmaBar_sub_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.Disorder.cstar M) * (√M.gamma)⁻¹)⁻¹ * 3 ^ (-(M.gamma * ↑n)))

What the state gives at the shifted index n − 2. The inverse form of sigmaBar_lower_of_inductionState at k = n − 2, with the exponent moved from 3^{γ(n−2)} to 3^{γn} at the honest cost 3^{2γ} ≤ 2.

This is the inverse form of the chain's (relaxed) hsignlow binder: the printed statement would give the constant 2 where this gives 4.

theorem Algsuperdiff.Section4.Provider.Annular.sigmaBar_ratio_le_four {d : ℕ} (M : Section3.ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) {m n : ℤ} (hnm : n - 2 ≤ m) (hm : m ≤ m0) : (↑(Section3.Annealed.sigmaBar M m))⁻¹ * ↑(Section3.Annealed.sigmaBar M (n - 2)) ≤ 4

The hratio slot at the constant 4. Both branches of e.shom.h.bounds at the two indices, with the max monotone in the scale.

Part C -- the hshell slot, at the explicit constant 196

theorem Algsuperdiff.Section4.Provider.Annular.shellBudget_of_eventG1_of_inductionState {d : ℕ} (M : Section3.ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) (m : ℤ) {s : ℝ} (hs0 : 0 ≤ s) (hs1 : s ≤ 1) {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG1 M m s (√(Section3.Disorder.cstar M) * (√M.gamma)⁻¹)) {n L : ℤ} (hnm : n ≤ m) (hmL : m ≤ L) (hn2 : n - 2 ≤ m0) {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) : (↑(Section3.Annealed.sigmaBar M (n - 2)))⁻¹ * (3 ^ (2 * ↑n) * Support.shellW1InfGradNorm n (Frozen.Assumptions.ShellField.translate (Support.triadicLatticePoint n v) (Section3.Provider.Stream.shellIncrement (↑omega) (n - 2) L))) ≤ 196 * 3 ^ (s / 4 * (↑m - ↑n))

The hshell slot of e.ugly.estimate.for.J, discharged. On the honest clause-(i) event 𝒢₁(m; s, √c⋆ γ^{−1/2}), for every L ≥ m and every scale-n lattice point z of □_m,

σ_{n−2}^{−1} · 3^{2n} ‖∇(k_L − k_{n−2})‖_{W^{1,∞}(z+□_n)} ≤ 196 · 3^{s(m−n)/4} .

A_sh = 196 is an absolute numeral: no s, no γ, no c⋆, no dimension. Two exact cancellations make this possible — the 𝒢₁ amplitude T' equals the chain's κ (gamma_mul_annularEventAmplitude_sq), and the gauge weight 3^{γn} is exactly the one the σ_{n−2} lower bound produces. The composition is 4 · 49: the 4 is inv_sigmaBar_sub_two_le_of_inductionState (the 2 times the 3^{2γ} ≤ 2 index shift), the 49 is ShellGaugeBudget.shellGauge_le_of_eventG1.