G2CubeBound

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

The per-cube two-term display of the 𝒢₂ atom (hcube)

ABK26, §4.1, Step 1 of l.ratio.of.good.scales.for.mathcal.E:

By Proposition p.induction.bounds, subadditivity of 𝓔, e.powerofGammasigma and e.maxy.bound …

This module discharges the first two of those four citations for the 𝒢₂ per-cube atom, i.e. it produces

𝓔_{s,2,2}(□_n; 𝐚_{n−2}, σ_{n−2}) ≤ 𝒪_{Γ_2}(A₁) + 𝒪_{Γ_{1/2}}(A₂)

— the hypothesis hcube of isTwoTermBigOWith_errorAnnMax. (The remaining two citations, e.powerofGammasigma and e.maxy.bound, are already performed in G2AtomTail.lean.)

The reading of the citation

The anchor Frozen.Section3.induction_bounds is stated at the diagonal triple (𝐚_m, □_m, σ_m) and at the exponent pair (∞,2); the 𝒢₂ atom needs the off-diagonal triple (𝐚_{n−2}, □_n, σ_{n−2}) at (2,2). Read at m:= n − 2, the anchor already carries the atom's coefficient scale and its comparator scale: 𝐚_{n−2} and σ_{n−2}. The only remaining discrepancy is the domain scale, n − 2 versus n, and that is exactly what "subadditivity of 𝓔" transports — from the 3^{2d} sub-cubes of □_n at scale n − 2 up to □_n itself. No field switch and no comparator switch occurs anywhere in the derivation.

The three ingredients:

• Support.homogenizationErrorOnCube_two_two_le_sqrt_three_mul — subadditivity of 𝓔 at (2,2), two scales up, at the numerical cost √3 (ErrorSwitch).
• BadEvents.homogenizationErrorOnCube_translateCutoffSample — the exponent- generic pathwise translation covariance, which turns the functional at a sub-cube into the functional at the centred cube read at a translated sample. This is stationarity, not a new estimate.
• isBigOWith_fmax at the machine-computed count #(descendants) = (3^d)^2 — e.maxy.bound over the sub-cubes. Its cost is the dimensional penalty annulusPenalty d σ 1 = (1 + 2d log 3)^{1/σ}, a constant.

Scope

Provider material: proved local helpers.

References

• ABK26, p.induction.bounds, e.subaddJ.nosymm, e.mathcalE.squared.max.bound.

The sub-cube count

The per-cube two-term display

theorem Algsuperdiff.Section4.Provider.Proportion.isTwoTermBigOWith_annularErrorObservable_of_diagonal {d : ℕ} (M : Section3.ABKModel d) {s : ℝ} (hs : 0 < s) (n : ℤ) {A1 A2 : ℝ} (hdiag : Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Section3.Observable.cutoffHomogenizationError M (n - 2) ⟨s, hs⟩) A1 A2) : Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Support.annularErrorObservable M n ⟨s, hs⟩) (√3 * (annulusPenalty d 2 1 * A1)) (√3 * (annulusPenalty d (1 / 2) 1 * A2))

The 𝒢₂ per-cube atom, from the anchor at the coefficient scale.

Given the two-term (Γ_2, Γ_{1/2}) display for the (∞,2) cutoff homogenization error at the DIAGONAL scale n − 2 — which is exactly what Frozen.Section3.induction_bounds supplies — the 𝒢₂ observable 𝓔_{s,2,2}(□_n; 𝐚_{n−2}, σ_{n−2}) obeys the same two-term display, with the amplitudes multiplied by √3 (subadditivity of 𝓔) and by the dimensional union-bound penalty over the (3^d)^2 sub-cubes.

The endpoint

theorem Algsuperdiff.Section4.Provider.Proportion.exists_isTwoTermBigOWith_annularErrorObservable (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (8 * M.gamma) 1) (n : ℤ), Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Support.annularErrorObservable M n ⟨s, ⋯⟩) (√3 * (annulusPenalty d 2 1 * (C * (Section3.Disorder.cstar M)⁻¹ * s⁻¹ * √M.gamma))) (√3 * (annulusPenalty d (1 / 2) 1 * Real.exp (-(C⁻¹ * Section3.Disorder.cstar M ^ 3 * M.gamma⁻¹))))

hcube, unconditionally, from the Section 3 anchor.

For every model in the printed regime γ ≤ C^{−10}c⋆^{10} and every s in the standing window [8γ, 1], the 𝒢₂ per-cube observable 𝓔_{s,2,2}(□_n; 𝐚_{n−2}, σ_{n−2}) obeys a two-term (Γ_2, Γ_{1/2}) display with amplitudes independent of n — the hypothesis hcube of isTwoTermBigOWith_errorAnnMax, isTwoTermBigOWith_Xcal and the 𝒢₂ moment engine.

The only hypotheses are the anchor's own: the dimensional constant C, the regime γ ≤ C^{−10}c⋆^{10} (the transfer gap, carried explicitly rather than assumed away) and the window s ∈ [8γ, 1].