ShellGaugeBudget

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

The 𝒢₁ gradient-gauge budget of Step 2, at the honest amplitude

ABK26, Section 4.1, p.mathcalE.annular.decomp Step 2. The manuscript's second good-event budget reads

σ_{n−2}^{-1} 3^{2n} sup_{L ≥ m} ‖∇(k_L − k_{n−2})‖_{W^{1,∞}(z+□_n)} 1_{𝒢}
  ≤ C 3^{s(m−n)/4} ,

and is the hshell slot of Ugly.uglyJEstimate_of_sensitivity, UglyChain.exists_responseJ_ugly_estimate and UglyLatticeChain.exists_uglyJEstimate_lattice_cube. This module produces the gauge half of it — everything except the σ prefactor — from membership in the frozen event Support.eventG1 M m s T, at an explicit numeral constant.

The decay the proved layer bound throws away

EventBudgets.three_rpow_mul_shellW1InfGradNorm_translate_le_shellBlockLatticeReal bounds the weighted layer term by 9 A(l) uniformly in l. That is enough for Step 3's Cauchy--Schwarz-with-multiplicity, but not for Step 2: summing a uniform bound over the (m−n)+2 layers costs a factor (m−n)+2, which no fixed power of 3^{s(m−n)/4} absorbs at a constant independent of s (the optimum is s^{-1/2}). The manuscript avoids this — keeps the factor 3^{(1−γ)(n−k)} through the cube comparison and only then applies Cauchy--Schwarz. three_rpow_gauge_weight_decay_le below is that sharper weight arithmetic; it retains the geometric decay and the layer sum is then bounded by an absolute constant, with no s-dependence anywhere.

What is proved

• three_rpow_gauge_weight_decay_le — the sharpened Step-2 weight arithmetic, at the constant 3 (both branches are tight at l = n − 1).
• three_rpow_mul_shellW1InfGradNorm_translate_le_decay — the per-layer bound with the decay retained.
• sum_three_rpow_decay_le — the layer sum of the decay weights is at most 8.
• shellBlockLatticeReal_le_of_eventG1 — the single-block reading of 𝒢₁ᵇ: every shell block in the layer range is at most 2 T 3^{s(m−n)/8}.
• shellGaugeHead_le_of_eventG1 / shellGaugeTail_le_of_eventG1 / shellGauge_le_of_eventG1 — the head block (n−2, m], the tail block (m, L] and their sum.

Part A -- the sharpened weight arithmetic, over abstract reals

theorem Algsuperdiff.Section4.Provider.Annular.three_rpow_gauge_weight_decay_le {gam nn ll : ℝ} (hl : nn - 1 ≤ ll) : 3 ^ ((2 - gam) * nn) * max 1 (3 ^ (ll - nn)) ≤ 3 * (3 ^ ((1 - gam) * (nn - ll)) * 3 ^ ((2 - gam) * ll))

The Step-2 weight arithmetic with the shell decay retained. For a layer index ll at or above nn − 1 — the honest range of the layer sum (n−2, m] — the cube-comparison factor max(1, 3^{ll−nn}) is paid for by the constant 3 and the geometric factor 3^{(1−gam)(nn−ll)} is kept:

3^{(2−gam) nn} max(1, 3^{ll−nn}) ≤ 3 · 3^{(1−gam)(nn−ll)} · 3^{(2−gam) ll} .

The second branch is an identity up to the constant; the first branch is tight at ll = nn − 1. Neither branch uses a bound on gam.

Part B -- the per-layer bound at the pinned lattice family

theorem Algsuperdiff.Section4.Provider.Annular.three_rpow_mul_shellW1InfGradNorm_translate_le_decay {d : ℕ} (M : Section3.ABKModel d) {m n l : ℤ} (hnm : n ≤ m) (hln : n - 1 ≤ l) (hlm : l ≤ m) (omega : Section3.Cutoff.CutoffSample d) {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) : 3 ^ ((2 - M.gamma) * ↑n) * Support.shellW1InfGradNorm n (Frozen.Assumptions.ShellField.translate (Support.triadicLatticePoint n v) (↑omega l)) ≤ 3 * (3 ^ ((1 - M.gamma) * (↑n - ↑l)) * shellBlockLatticeReal M m omega l)

The per-shell atom bound with the decay retained. On the cube z + □_n with z a scale-n lattice point of □_m, the weighted W^{1,∞} gauge of the shell j_l is at most 3 · 3^{(1−γ)(n−l)} A(l), with A = shellBlockLatticeReal the pinned lattice family of the frozen clause-(i) fourth term. This is the sharpening of EventBudgets.three_rpow_mul_shellW1InfGradNorm_translate_le_shellBlockLatticeReal that Step 2 needs.

Part C -- the layer sum of the decay weights

theorem Algsuperdiff.Section4.Provider.Annular.sum_three_rpow_decay_le {d : ℕ} (M : Section3.ABKModel d) {n m : ℤ} (hnm : n ≤ m) : ∑ l ∈ Finset.Icc (n - 1) m, 3 ^ ((1 - M.gamma) * (↑n - ↑l)) ≤ 8

The layer sum of the decay weights is bounded by an absolute constant. Over the honest layer range l ∈ [n−1, m] the geometric factors of three_rpow_gauge_weight_decay_le sum to at most 8, uniformly in n, m and in γ ≤ 1/4. This is the step that keeps the Step-2 budget free of s.

Part D -- the single-block reading of 𝒢₁ᵇ

theorem Algsuperdiff.Section4.Provider.Annular.shellBlockLatticeReal_le_of_eventG1 {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) {s T : ℝ} (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (hT : 0 ≤ T) {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG1 M m s T) {n l : ℤ} (hnm : n ≤ m) (hln : n - 1 ≤ l) (hlm : l ≤ m) : shellBlockLatticeReal M m omega l ≤ 2 * T * 3 ^ (s / 8 * ↑(m - n))

The single-block reading of 𝒢₁ᵇ. On 𝒢₁(m; s, T) every shell block in the layer range [n−1, m] of the annulus at scale n is at most 2 T 3^{s(m−n)/8}. Unlike EventReading.shellPartialSum_le_of_eventG1 this is a bound on a single block, at the first power, which is what the Step-2 layer sum consumes.

Part E -- the head block (n−2, m]

theorem Algsuperdiff.Section4.Provider.Annular.shellGaugeHead_le_of_eventG1 {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) {s T : ℝ} (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (hT : 0 ≤ T) {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG1 M m s T) {n : ℤ} (hnm : n ≤ m) {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) : 3 ^ ((2 - M.gamma) * ↑n) * Support.shellW1InfGradNorm n (Frozen.Assumptions.ShellField.translate (Support.triadicLatticePoint n v) (Section3.Provider.Stream.shellIncrement (↑omega) (n - 2) m)) ≤ 48 * T * 3 ^ (s / 8 * ↑(m - n))

The head block of the Step-2 gauge budget. On 𝒢₁(m; s, T) the weighted W^{1,∞} gauge of ∇(k_m − k_{n−2}) on the lattice cube z + □_n is at most 48 T 3^{s(m−n)/8}. The constant is absolute: 3 from the weight arithmetic, 8 from the layer sum of the decay weights and 2 from the single-block reading of 𝒢₁ᵇ.

Part F -- the tail block (m, L] and the raw tail summability

theorem Algsuperdiff.Section4.Provider.Annular.sum_gradTailFam_Ioc_le_tsum {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) {s T : ℝ} {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG1 M m s T) (b : ℤ) : 3 ^ ((2 - M.gamma) * ↑m) * ∑ l ∈ Finset.Ioc m b, Support.shellW1InfGradNorm m (↑omega l) ≤ ∑' (k : { k : ℤ // m ≤ k }), 3 ^ ((2 - M.gamma) * ↑m) * Support.shellW1InfGradNorm m (↑omega ↑k)

The weighted layer sum over (m, b] sits below the full 𝒢₁ᵃ tail sum, i.e. below √(gradTailSq). This is the form the fifth (gradM) slot of e.ugly.estimate.for.J consumes.

theorem Algsuperdiff.Section4.Provider.Annular.shellGaugeTail_le_tsum_of_eventG1 {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) {s T : ℝ} {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG1 M m s T) {n L : ℤ} (hnm : n ≤ m) {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) : 3 ^ ((2 - M.gamma) * ↑n) * Support.shellW1InfGradNorm n (Frozen.Assumptions.ShellField.translate (Support.triadicLatticePoint n v) (Section3.Provider.Stream.shellIncrement (↑omega) m L)) ≤ ∑' (k : { k : ℤ // m ≤ k }), 3 ^ ((2 - M.gamma) * ↑m) * Support.shellW1InfGradNorm m (↑omega ↑k)

The tail block of the Step-2 gauge budget. The layers above m are transported to scale m by the cross-scale comparison and then absorbed by the first component of 𝒢₁, with constant 1. No relation between m and L is needed: for L < m the layer range is empty.

theorem Algsuperdiff.Section4.Provider.Annular.shellGaugeTail_le_of_eventG1 {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) {s T : ℝ} (hT : 0 ≤ T) {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG1 M m s T) {n L : ℤ} (hnm : n ≤ m) {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) : 3 ^ ((2 - M.gamma) * ↑n) * Support.shellW1InfGradNorm n (Frozen.Assumptions.ShellField.translate (Support.triadicLatticePoint n v) (Section3.Provider.Stream.shellIncrement (↑omega) m L)) ≤ T

The tail block of the Step-2 gauge budget, against the event threshold.

Part G -- the full Step-2 gauge bound

theorem Algsuperdiff.Section4.Provider.Annular.shellGauge_le_of_eventG1 {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) {s T : ℝ} (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (hT : 0 ≤ T) {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG1 M m s T) {n L : ℤ} (hnm : n ≤ m) (hmL : m ≤ L) {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) : 3 ^ ((2 - M.gamma) * ↑n) * Support.shellW1InfGradNorm n (Frozen.Assumptions.ShellField.translate (Support.triadicLatticePoint n v) (Section3.Provider.Stream.shellIncrement (↑omega) (n - 2) L)) ≤ 49 * T * 3 ^ (s / 8 * ↑(m - n))

The Step-2 gauge budget, gauge half. On 𝒢₁(m; s, T), for every L ≥ m and every scale-n lattice point of □_m,

3^{(2−γ)n} ‖∇(k_L − k_{n−2})‖_{W^{1,∞}(z+□_n)} ≤ 49 T 3^{s(m−n)/8} .

The constant 49 = 48 + 1 is absolute: no s, no γ, no c⋆, no dimension.