ErrorSlotB4

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

B4 at the Step-3 shell cube: the two-scale (2,2) error display

What this module does

Bullet (B4) quotes p.induction.bounds at the off-diagonal triple (𝓔_{s,2,2}, □_j, 𝐚_{j−2}, shom_{j−2}) while the proposition is proved at the diagonal triple and at the exponent pair (∞,2).

That gap is already closed in the Section-4 material proved here, and this module records the exact handle and lifts it to the cube family the Step-3 shell actually uses:

• the index shift and the exponent switch are Proportion.exists_isTwoTermBigOWith_annularErrorObservable, which reads the Frozen.Section3.induction_bounds at m := j − 2 (so the coefficient scale 𝐚_{j−2} AND the comparator scale σ_{j−2} are the anchor's own) and lifts the DOMAIN scale from j − 2 to j through Support.homogenizationErrorOnCube_two_two_le_sqrt_three_mul (subadditivity of 𝓔 at the finite spatial exponent, cost √3) and the maximum lemma over the (3^d)^2 sub-cubes (cost Proportion.annulusPenalty d σ 1, a d-constant);
• the passage from the O cube □_j to the Step-3 shell cube 3^j v + □_j is stationarity: isTwoTermBigOWith_comp_translateCutoffSample below carries a two-term display along any real translation of the sample, because both witnesses are carried by the proved one-term transport Stream.isBigOWith_comp_translateCutoffSample.

What is NOT claimed

No moment conversion is performed here: bullet (B4)'s "hence, for every q ∈ [1,∞)" line (e.moments.OGamma2) is a separate Step-4 item.

References

• ABK26, (bullet (B4)), (p.induction.bounds), (e.mathcalE.squared.max.bound).

1. Two-term displays travel along real translations of the sample

theorem Algsuperdiff.Section4.Provider.BoundsEaL.isTwoTermBigOWith_comp_translateCutoffSample {d : ℕ} (M : Section3.ABKModel d) (z : HCPolySupport.Vec d) {Psi1 Psi2 : ℝ → ℝ} {X : Section3.Cutoff.CutoffSample d → ℝ} {A1 A2 : ℝ} (h : Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) Psi1 Psi2 X A1 A2) : Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) Psi1 Psi2 (fun (omega : Section3.Cutoff.CutoffSample d) => X (Section3.Cutoff.translateCutoffSample z omega)) A1 A2

Stationarity for a two-term display. Both witnesses of a Probability.IsTwoTermBigOWith are ordinary one-term weak-Orlicz bounds, and the cutoff-sample law is invariant under every real translation, so the whole display holds verbatim for the observable read at the translated sample.

2. B4 at the Step-3 shell cube

theorem Algsuperdiff.Section4.Provider.BoundsEaL.exists_isTwoTermBigOWith_annularErrorObservable_translate (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) (R : HCPolySupport.TriadicCube d), Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (fun (omega : Section3.Cutoff.CutoffSample d) => Support.annularErrorObservable M R.scale ⟨s, ⋯⟩ (Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint R.scale R.index) omega)) (√3 * (Proportion.annulusPenalty d 2 1 * (C * (Section3.Disorder.cstar M)⁻¹ * s⁻¹ * √M.gamma))) (√3 * (Proportion.annulusPenalty d (1 / 2) 1 * Real.exp (-(C⁻¹ * Section3.Disorder.cstar M ^ 3 * M.gamma⁻¹))))

Bullet (B4) at every Step-3 shell cube.

For every model in the anchor's regime and every s in its window, the (2,2) homogenization error on the cube 3^j v + □_j with the coefficient field 𝐚_{j−2} and the comparator σ_{j−2} obeys a two-term (Γ₂, Γ_{1/2}) display with amplitudes independent of the cube -- the printed 𝒪_{Γ₂}(C s^{-1} γ^{1/2}) + 𝒪_{Γ_{1/2}}(exp(−C^{-1} γ^{-1})), with the manuscript's C(d, c⋆) convention absorbing the explicit √3 · annulusPenalty d σ 1 · c⋆-factors carried here.

3. The a.e. bridge to the literal (2,2) error

theorem Algsuperdiff.Section4.Provider.BoundsEaL.ae_eq_annularErrorObservable_translate {d : ℕ} (M : Section3.ABKModel d) (R : HCPolySupport.TriadicCube d) (s : { s : ℝ // 0 < s }) : (fun (omega : Section3.Cutoff.CutoffSample d) => Frozen.Section24.unitCubeHomogenizationError (↑s) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Section3.Provider.BadEvents.unitRescaledCutoffCoeff M R (R.scale - 2) omega) (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M (R.scale - 2)))) =ᵐ[↑(Section3.Cutoff.cutoffSampleLaw M)] fun (omega : Section3.Cutoff.CutoffSample d) => Support.annularErrorObservable M R.scale s (Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint R.scale R.index) omega)

The literal (2,2) error of the Step-3 shell agrees almost everywhere with the observable of the display above. This is the honest interface: the literal object is a.e. measurable only, so it can carry the display only through this identification.