LambdaBudget

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

The hlam budget, discharged from 𝒢₀

ABK26, Section 4.1, p.mathcalE.annular.decomp Step 2. The ugly chain's λ-budget is

σ_{n−2} · λ_{s,2}^{-1}(z+□_n; a_{n−2}) ≤ C_l 3^{γ(m−n)} ,
    z = 3^n v ,  s = 2γ  (the gapped gauge).

𝒢₀(m) controls λ_{γ,2}^{-1} only at domain scale = cutoff scale = n−2 and only at the annulus lattice positions 3^{n−2}ℤ^d ∩ (□_m ∖ □_n). Three steps close the gap, and a fourth is a genuine obstruction:

1. The gauge. Localize.inv_lambdaSq_two_antitone_gauge transports the event's γ-gauge control to the gapped gauge 2γ at constant 1. This is the only available direction.
2. The domain. lambdaSq_finite_two_inv_le_nine_pow_mul_max_descendants_sub_two raises the domain from n−2 to n at the same exponent, at the constant 1 + 9^d·3^{−4γ} ≤ 1 + 9^d.
3. The coverage (index_mem_latticeAnnulusSet_of_mem_descendantsAtScale). Every scale-(n−2) descendant of z+□_n has its base point in □_m ∖ □_n — hence at an index 𝒢₀ actually controls — provided v ≠ 0. The containment in □_m is the tiling of □_m by the scale-n lattice cubes; the exclusion from □_n is the disjointness of distinct scale-n cubes.
4. The σ index. 𝒢₀'s bracket carries σ_{n−3} while the budget needs σ_{n−2}; the induction state gives σ_{n−2} ≤ 8 σ_{n−3} (sigmaBar_sub_two_le_eight_mul_sigmaBar_sub_three).

The uncovered class

At v = 0 the cube is the centred cube □_n, and every one of its 9^d scale-(n−2) descendants has its base point inside □_n (those base points are 3^{n−2} w with |w_i| ≤ 4 < 9/2). 𝒢₀ therefore says nothing at all about λ^{-1}(□_n; a_{n−2}), at any k: its own supremum only ever reaches the annulus □_m ∖ □_k, and only k = n produces the field index n−2.

This is not a gap in the ugly chain: the consumer never needs v = 0. The chain applies the budget only at annulus indices v ∈ 3^nℤ^d ∩ (□_j ∖ □_{j−1}) with n ≤ j−1, and □_n ⊆ □_{j−1} forces 3^n v ∉ □_n, i.e. v ≠ 0. The hlam binder of the chain is therefore stated at Support.latticeAnnulusSet d n m n — the manuscript's own annulus indexing — which is a strictly weaker hypothesis than Support.latticeCubeSet d n m and is exactly what the consumer supplies.

References

• ABK26, p.mathcalE.annular.decomp Step 2.
• d.good.event.for.lambda, (𝒢₀).

Part A -- the coverage geometry

theorem Algsuperdiff.Section4.Provider.Annular.descendantsAtScale_latticeCube_sub_two_data {d : ℕ} {n : ℤ} {v : Fin d → ℤ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (latticeCube n v) (n - 2)) : R.scale = n - 2 ∧ ∀ (i : Fin d), 2 * |R.index i - 9 * v i| < 9

The scale and index box of a scale-(n−2) descendant of the scale-n lattice cube: the index sits within 4 of 9 v.

theorem Algsuperdiff.Section4.Provider.Annular.descendantsAtScale_latticeCube_sub_two_nonempty {d : ℕ} (n : ℤ) (v : Fin d → ℤ) : (HCPolySupport.descendantsAtScale (latticeCube n v) (n - 2)).Nonempty

The scale-(n−2) descendants of a scale-n cube are never empty: the central one, at index 9 v, is always there.

theorem Algsuperdiff.Section4.Provider.Annular.index_mem_latticeAnnulusSet_of_mem_descendantsAtScale {d : ℕ} {n m : ℤ} (hnm : n ≤ m) {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) (hv0 : v ≠ 0) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (latticeCube n v) (n - 2)) : R.index ∈ Support.latticeAnnulusSet d (n - 2) m n

The coverage step. For a scale-n lattice cube of □_m that is not the centred one, every scale-(n−2) descendant sits at a lattice index of the annulus □_m ∖ □_n — precisely the index family 𝒢₀(m) controls at k = n.

v ≠ 0 is necessary and not merely convenient: at v = 0 all 9^d descendants have |index| ≤ 4, hence base point inside □_n, and 𝒢₀ reaches none of them (module docstring).

theorem Algsuperdiff.Section4.Provider.Annular.ne_zero_of_mem_latticeAnnulusSet {d : ℕ} {n m : ℤ} {v : Fin d → ℤ} (hv : v ∈ Support.latticeAnnulusSet d n m n) : v ≠ 0

The centred cube is the only scale-n lattice cube whose base point lies in □_n; hence an annulus index is nonzero.

Part B -- the descendant atom, read off 𝒢₀

theorem Algsuperdiff.Section4.Provider.Annular.inv_lambdaSq_latticeCube_le_of_mem_eventG0 {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) {m n : ℤ} (hn : n ≤ m - 1) {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG0 M Ccg m) {w : Fin d → ℤ} (hw : w ∈ Support.latticeAnnulusSet d (n - 2) m n) : (HCPolySupport.Book.Ch02.lambdaSq (latticeCube (n - 2) w) M.gamma (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Section3.Cutoff.coefficientCutoffTriadicCoeffFamily M (n - 2) omega))⁻¹ ≤ (↑(Section3.Annealed.sigmaBar M (n - 3)))⁻¹ * (Ccg + 3 ^ (1 / 4 * M.gamma * ↑(m - n)))

The 𝒢₀ reading at one annulus descendant. For an annulus lattice index w of □_m ∖ □_n, the λ_{γ,2}^{-1} of the scale-(n−2) cube at w, read at the cutoff field a_{n−2}, is at most σ_{n−3}^{-1}(C_cg + 3^{γ(m−n)/4}). This is 𝒢₀'s own inequality at the single index k = n, rearranged.

Part C -- the one-step σ ratio

theorem Algsuperdiff.Section4.Provider.Annular.sigmaBar_sub_two_le_eight_mul_sigmaBar_sub_three {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)) ≤ 8 * ↑(Section3.Annealed.sigmaBar M (n - 3))

The one-step running-diffusivity ratio. Both branches of e.shom.h.bounds at the two consecutive indices, with the shift 3^{2γ} ≤ 2 supplied by the standing γ ≤ 1/4. This converts 𝒢₀'s σ_{n−3} bracket into the budget's σ_{n−2} at the absolute numeral 8.

Part D -- the hlam display

def Algsuperdiff.Section4.Provider.Annular.annularLambdaConstant (d : ℕ) (Ccg : ℝ) : ℝ

The hlam constant: 8 (1 + 9^d)(1 + C_cg). The 8 is the one-step σ ratio, the 1 + 9^d is the cube-raising at separation 2 (its sharp value `1

• 9^d 3^{−4γ}is only relaxed here), and the1 + C_cgis the𝒢₀bracket. Dimension andC_cgonly: nos, no γ, no c⋆`.

Equations

• Algsuperdiff.Section4.Provider.Annular.annularLambdaConstant d Ccg = 8 * (1 + 9 ^ d) * (1 + Ccg)

theorem Algsuperdiff.Section4.Provider.Annular.annularLambdaConstant_nonneg (d : ℕ) {Ccg : ℝ} (hCcg : 0 ≤ Ccg) : 0 ≤ annularLambdaConstant d Ccg

theorem Algsuperdiff.Section4.Provider.Annular.sigmaBar_mul_inv_unitCubeLambda_two_gamma_le_of_mem_eventG0 {d : ℕ} [NeZero d] (M : Section3.ABKModel d) {Ccg : ℝ} (hCcg : 0 ≤ Ccg) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) {m n : ℤ} (hn : n ≤ m - 1) (hn2 : n - 2 ≤ m0) {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG0 M Ccg m) {v : Fin d → ℤ} (hv : v ∈ Support.latticeAnnulusSet d n m n) : ↑(Section3.Annealed.sigmaBar M (n - 2)) * (Frozen.Section24.unitCubeLambda (2 * M.gamma) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Section3.Provider.BadEvents.unitRescaledCutoffCoeff M { scale := n, index := v } (n - 2) omega))⁻¹ ≤ annularLambdaConstant d Ccg * 3 ^ (M.gamma * (↑m - ↑n))

The hlam budget, discharged at the gapped gauge s = 2γ, on 𝒢₀(m) and at every annulus lattice cube of □_m ∖ □_n.

The four steps are the gauge antitonicity, the cube-raising bound of LambdaMatrixRoute, the coverage step proved above, and the one-step σ ratio; the constant is annularLambdaConstant d C_cg = 8(1+9^d)(1+C_cg), and the printed weight 3^{γ(m−n)} is unchanged (the event supplies only 3^{γ(m−n)/4}, so three quarters of the printed discount is left on the table).

v ≠ 0 — carried here as v ∈ latticeAnnulusSet d n m n — is essential: see the module docstring for the exact uncovered class.