EightEss

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

The e.mathcal.E.eight.ess.bound opening: unfolding the (∞,2) error

ABK26, Section 4.1: the first display of the proof of p.mathcalE.annular.decomp opens

E_{s,∞,2}(□_m; ã_{L,m}, σ_m)^2
  ≤ C c_{2s} Σ_{n≤m} 3^{-2s(m-n)} max_{z ∈ 3^n Z^d ∩ □_m} max_{|e|=1}
        J(z+□_n, σ_m^{-1/2} e, σ_m^{1/2} e; ã_{L,m})
    + (the same with the transposed field) .

This module produces the exact left-hand identity at the proved observable layer and reduces the display to its two genuine inputs.

What is proved

fluxCorrectedError_sq_eq_scaleSum is an identity, not an estimate:

fluxCorrectedError M L m s ω ^ 2
  = c_{2s} Σ_{l ≥ 0} 3^{-2 s l}
      · maxDescendantNormalizedBlockResponse (□_m at depth l) (ã_{L,m}) (σ_m Id) ,

with the manuscript's own normalizing factor c_{2s} = 1 - 3^{-2s} explicit and the scale index l = m - n, so the geometric weight is literally 3^{-2s(m-n)}. This is the proved Ch02.homogenizationErrorOnCube_infinity_two_sq_eq_tsum transported along Support.fluxCorrectedError_characterization.

What is slotted, and why

Two conversions separate the identity above from the printed display, and N is available in the repository today:

1. e.bfJ.general -- the inner quantity is normalizedBlockResponseMax, a maximum of the doubled response over the full-block unit sphere of 2d dimensions. The printed display replaces it by the half-sum of the scalar J at the pair (σ_m^{-1/2}e, σ_m^{1/2}e) for the field and for its transpose. The proved responseJ_scalarLoading_le_normalizedBlockResponseMax runs in the O direction (J ≤ block max), so this conversion is a genuine missing input.
2. The descendant-vs-lattice identification -- the inner maximum runs over descendantsAtScale □_m (m-l), the triadic descendants of □_m; the manuscript's maximum runs over the lattice points 3^n Z^d ∩ □_m. The two enumerate the same cubes, but no lemma identifies them (Support.latticeCubeSet carries no proved lemma at all).

eightEss_of_blockResponse_le therefore takes both, jointly, as the single named hypothesis hbfJ -- exactly the graph's e.bfJ.general edge -- and delivers the printed two-term display.

The geometric weight in the manuscript's spelling

theorem Algsuperdiff.Section4.Provider.Annular.geometricWeight_two_eq (s : ℝ) (l : ℕ) : HCPolySupport.Book.Ch02.geometricWeight s 2 l = (1 - 3 ^ (-(2 * s))) * 3 ^ (-(2 * s) * ↑l)

The q = 2 geometric weight of the (∞,2) error is the manuscript's c_{2s} 3^{-2 s l} (the factor written 𝔠_{2s}).

The exact scale-sum identity

theorem Algsuperdiff.Section4.Provider.Annular.fluxCorrectedError_sq_eq_scaleSum {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) {s : ℝ} (hs : 0 < s) (omega : Section3.Cutoff.CutoffSample d) : Support.fluxCorrectedError M L m s omega ^ 2 = ∑' (l : ℕ), HCPolySupport.Book.Ch02.geometricWeight s 2 l * HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale (HCPolySupport.originCube d m) (m - ↑l) (Support.fluxCorrectedCoeffFamily M L m (HCPolySupport.originCube d m) omega) (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M m))

The (∞,2) opening as an identity.

The squared flux-corrected error is exactly the c_{2s}-normalized geometric scale sum of the descendant maxima of the normalized block response. The summation index l is the manuscript's m - n.

theorem Algsuperdiff.Section4.Provider.Annular.fluxCorrectedError_sq_eq_normalized {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) {s : ℝ} (hs : 0 < s) (omega : Section3.Cutoff.CutoffSample d) : Support.fluxCorrectedError M L m s omega ^ 2 = (1 - 3 ^ (-(2 * s))) * ∑' (l : ℕ), 3 ^ (-(2 * s) * ↑l) * HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale (HCPolySupport.originCube d m) (m - ↑l) (Support.fluxCorrectedCoeffFamily M L m (HCPolySupport.originCube d m) omega) (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M m))

The same identity with the manuscript's c_{2s} pulled out of the sum.

The two-term display

theorem Algsuperdiff.Section4.Provider.Annular.eightEss_of_blockResponse_le {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) {s C : ℝ} (hs : 0 < s) (omega : Section3.Cutoff.CutoffSample d) {Jfld Jtrn : ℕ → ℝ} (hbfJ : ∀ (l : ℕ), HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale (HCPolySupport.originCube d m) (m - ↑l) (Support.fluxCorrectedCoeffFamily M L m (HCPolySupport.originCube d m) omega) (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M m)) ≤ C * (Jfld l + Jtrn l)) (hsumF : Summable fun (l : ℕ) => 3 ^ (-(2 * s) * ↑l) * Jfld l) (hsumT : Summable fun (l : ℕ) => 3 ^ (-(2 * s) * ↑l) * Jtrn l) : Support.fluxCorrectedError M L m s omega ^ 2 ≤ C * (1 - 3 ^ (-(2 * s))) * ∑' (l : ℕ), 3 ^ (-(2 * s) * ↑l) * Jfld l + C * (1 - 3 ^ (-(2 * s))) * ∑' (l : ℕ), 3 ^ (-(2 * s) * ↑l) * Jtrn l

e.mathcal.E.eight.ess.bound, modulo e.bfJ.general.

Given the conversion of the descendant block-response maximum into the manuscript's two lattice J-maxima -- the field term Jfld and the transpose term Jtrn, at the constant C -- the printed two-term display follows, with c_{2s} explicit.

hbfJ is the graph's e.bfJ.general edge together with the descendant-vs- lattice identification; both are recorded frontier inputs, not proved here.