Breakdown

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

Provider: the localization breakdown e.mathcal.E.breakdown

This file is a proved local provider for the display e.mathcal.E.breakdown of ABK26, the first displayed step in the proof of the localization lemma l.localization.mathcalE. It is a provider endpoint only: the localization lemma itself additionally needs the comparator normalization, the λ-gate, the J-injection, the good-event aggregation and the bad-event factorization, none of which is in this file.

Applying e.mathcalE.infty.to.q with p = 2ds^{-1} and q = 2 and squaring, the source records

`𝓔_{s,∞,2}(□m; a_m, σ_m)^2 ≤ c{2s} Σ_{l=-∞}^m 3^{-s(m-l)} (⨍_{z ∈ 3^l ℤ^d ∩ □m} max{|e|=1} J(z+□_l, σ_m^{-1/2}e, σ_m^{1/2}e; a_m)^{d/s})^{s/d}

• c_{2s} Σ_{l=-∞}^m 3^{-s(m-l)} (⨍_{z ∈ 3^l ℤ^d ∩ □m} max{|e|=1} J(z+□_l, σ_m^{-1/2}e, σ_m^{1/2}e; a_m^t)^{d/s})^{s/d}`,

where c_{2s} = 1 - 3^{-2s} is Homogenization.Book.Ch02.geometricDiscount s 2.

Main results

• homogenizationErrorOnCube_sq_le_breakdown: the display, pathwise on CoarseGraining's literal 𝓔_{s,∞,2} carrier, for every triadic coefficient family and every constant comparator. The two right-hand terms carry the coefficient (1/2) c_{2s}: the 1/2 is the weight of the block splitting, retained rather than discarded, and it cancels the doubling of the frame-sup legs, so that the conclusion is the printed display verbatim under the leg identification legA = 2 · max_{|e|=1} J(·; a) (see the frame-sup deviation below).
• cutoffHomogenizationError_sq_ae_le_breakdown: the same display transported to the Section 3 observable Observable.cutoffHomogenizationError M m ⟨s, _⟩ at the running diffusivity σ_m.
• breakdownLegA / breakdownLegB, legScaleAverage, breakdownLegSum: the two legs and the two weighted leg sums of the display, with the A (responseJ_le_breakdownLegA, breakdownLegA_le_of_forall_frame, legScaleAverage_smul, summable_breakdownLegSum_terms, and their B twins) through which the downstream comparator normalization consumes the conclusion.
• breakdownLegAValueSet_isotropic_eq / breakdownLegBValueSet_isotropic_eq and breakdownLegA_le_of_paired_bound / breakdownLegB_le_of_paired_bound: at the isotropic comparator σ Id — the only comparator on the localization wire — the two legs are exactly the manuscript's paired families J(z+□_l, σ^{-1/2}v, σ^{1/2}v; a) and J(z+□_l, σ^{-1/2}v, σ^{1/2}v; a^t) at v = e₁ ∓ e₂, with |v|^2 ≤ 2 (vecNormSq_frameLegAVec_le, vecNormSq_frameLegBVec_le). The loadings are written in the Section 3 carrier's own spelling Observable.inverseSqrtLoad / Observable.sqrtLoad.

Source correspondence and disclosed deviations

• d.mathcal.E is built from the block functional 𝐉(R, 𝐀_0^{-1/2}e, 𝐀_0^{1/2}e; a) with e a unit vector of the doubled 2d-dimensional space; the two scalar legs of the printed display arise from it through the unconditional block splitting doubledResponseJ = ½ J(·;a) + ½ J(·;a^t) (Homogenization.Book.Ch02.doubledResponseJ_eq_half_responseJ_adjoint_sum). Accordingly breakdownLegA / breakdownLegB are the suprema of the scalar responses over the doubled unit sphere; at the scalar comparator used on the localization wire the loading vector v = e₁ ∓ e₂ has Euclidean length up to √2, so each leg is twice the printed max_{|e|=1} object. This file carries the frame-sup form. The doubling and the 1/2 of the splitting cancel here, and the cancellation is performed rather than asserted. The 1/2 of doubledResponseJ = ½ J(·;a) + ½ J(·;a^t) is retained in normalizedBlockResponseMax_le_breakdownLegA_add_breakdownLegB (which is therefore a bound by ½ (legA + legB), not by legA + legB), and it is carried through the per-scale power mean by its positive homogeneity (legScaleAverage_smul) into the constant of both endpoints. The paired shape and the size bound |v|^2 ≤ 2 are proved here at the isotropic comparator (breakdownLegAValueSet_isotropic_eq and its twin), so the deviation is exhibited rather than asserted. What the cancellation removes is the second, spurious factor 2 — the one that came from the discarded splitting weight and had no source warrant at all.
• The gap is an artifact of the printed range, not of the mathematics: what the breakdown actually needs from the embedding is its one-scale counting core, which carries no window on s at all. This file therefore consumes ErrorComparison.scaleResponseAtScale_infinity_rpow_le_card_mul_finite (binders 0 < p, 0 < q only) and performs the outer geometric scale sum directly, rather than the packaged display ErrorComparison.homogenizationError_infinity_le_finite, whose retained (and, in that file, unused) binder s < 1 would exclude the endpoint. The resulting statement holds on all of s ∈ (0, 1], so the recorded source gap is refuted in Lean rather than inherited.
• Consequently the inner and outer power-mean exponents are the printed d/s and s/d, and the geometric weight is the printed 3^{-s(m-l)}.
• No 𝓔_{s,p,∞} branch and no n < m truncation occurs.
• The deterministic statement homogenizationErrorOnCube_sq_le_breakdown is genuinely pathwise: it holds for every coefficient family and every comparator, with no exceptional set. The Section 3 endpoint is nevertheless almost sure, and its null set sits inside the s binder, because the observable Observable.cutoffHomogenizationError is an verified measurable representative which only almost everywhere equals CoarseGraining's literal 𝓔_{s,∞,2} (Observable.cutoffHomogenizationError_ae_eq_homogenizationErrorOnCube), and that identification is itself indexed by s. The a.e. quantifier here is therefore forced by the carrier, not by the argument; the s-uniform form would require an s-uniform representative identification, which the Observable layer does not supply.

References

• ABK26, e.mathcal.E.breakdown, inside l.localization.mathcalE.
• ABK26, e.mathcalE.infty.to.q (d.mathcal.E).

Real-power and finite-average bookkeeping

The two frame legs of the display

noncomputable def Algsuperdiff.Section3.Provider.Localization.frameLoadInvSqrt {d : ℕ} (a0 : HCPolySupport.Mat d) (e : HCPolySupport.FullBlockVec d) : HCPolySupport.BlockVec d

The block-normalized loading 𝐀_0^{-1/2} e of a doubled direction e, split into its two ℝ^d halves.

Equations

• Algsuperdiff.Section3.Provider.Localization.frameLoadInvSqrt a0 e = HCPolySupport.ofFullBlockVec (Matrix.mulVec (HCPolySupport.Book.Ch02.constantFullBlockMatrixInvSqrt a0) e)

noncomputable def Algsuperdiff.Section3.Provider.Localization.frameLoadSqrt {d : ℕ} (a0 : HCPolySupport.Mat d) (e : HCPolySupport.FullBlockVec d) : HCPolySupport.BlockVec d

The block-normalized loading 𝐀_0^{1/2} e of a doubled direction e, split into its two ℝ^d halves.

Equations

• Algsuperdiff.Section3.Provider.Localization.frameLoadSqrt a0 e = HCPolySupport.ofFullBlockVec (Matrix.mulVec (HCPolySupport.Book.Ch02.constantFullBlockMatrixSqrt a0) e)

def Algsuperdiff.Section3.Provider.Localization.breakdownLegAValueSet {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) : Set ℝ

The value set of the a-leg of e.mathcal.E.breakdown: the scalar responses J(R, ·, ·; a) at the primal frame loadings of the doubled unit directions.

Equations

• One or more equations did not get rendered due to their size.

def Algsuperdiff.Section3.Provider.Localization.breakdownLegBValueSet {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) : Set ℝ

The value set of the a^t-leg of e.mathcal.E.breakdown: the scalar responses J(R, ·, ·; a^t) at the adjoint frame loadings of the doubled unit directions.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Localization.breakdownLegA {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) : ℝ

The a-leg of e.mathcal.E.breakdown: the frame supremum max_{|e|=1} J(R, 𝐀_0^{-1/2}e, 𝐀_0^{1/2}e; a) over the doubled unit sphere.

Equations

• Algsuperdiff.Section3.Provider.Localization.breakdownLegA R a a0 = sSup (Algsuperdiff.Section3.Provider.Localization.breakdownLegAValueSet R a a0)

noncomputable def Algsuperdiff.Section3.Provider.Localization.breakdownLegB {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) : ℝ

The a^t-leg of e.mathcal.E.breakdown: the frame supremum max_{|e|=1} J(R, 𝐀_0^{-1/2}e, 𝐀_0^{1/2}e; a^t) over the doubled unit sphere.

Equations

• Algsuperdiff.Section3.Provider.Localization.breakdownLegB R a a0 = sSup (Algsuperdiff.Section3.Provider.Localization.breakdownLegBValueSet R a a0)

theorem Algsuperdiff.Section3.Provider.Localization.breakdownLegA_nonneg {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) : 0 ≤ breakdownLegA R a a0

The a-leg is nonnegative.

theorem Algsuperdiff.Section3.Provider.Localization.breakdownLegB_nonneg {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) : 0 ≤ breakdownLegB R a a0

The a^t-leg is nonnegative.

theorem Algsuperdiff.Section3.Provider.Localization.breakdownLegAValueSet_bddAbove {d : ℕ} {Q R : HCPolySupport.TriadicCube d} {k : ℤ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) (hR : R ∈ HCPolySupport.descendantsAtScale Q k) : BddAbove (breakdownLegAValueSet R a a0)

On a descendant cube the a-leg value set is bounded above.

theorem Algsuperdiff.Section3.Provider.Localization.breakdownLegBValueSet_bddAbove {d : ℕ} {Q R : HCPolySupport.TriadicCube d} {k : ℤ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) (hR : R ∈ HCPolySupport.descendantsAtScale Q k) : BddAbove (breakdownLegBValueSet R a a0)

On a descendant cube the a^t-leg value set is bounded above.

theorem Algsuperdiff.Section3.Provider.Localization.responseJ_le_breakdownLegA {d : ℕ} {Q R : HCPolySupport.TriadicCube d} {k : ℤ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) (hR : R ∈ HCPolySupport.descendantsAtScale Q k) {e : HCPolySupport.FullBlockVec d} (he : HCPolySupport.Book.Ch02.fullBlockVecNormSq e = 1) : HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (a.coeffOn R) ((frameLoadInvSqrt a0 e).1 - (frameLoadSqrt a0 e).2) ((frameLoadSqrt a0 e).1 - (frameLoadInvSqrt a0 e).2) ≤ breakdownLegA R a a0

Every a-leg frame value of a descendant cube is bounded by the leg.

theorem Algsuperdiff.Section3.Provider.Localization.responseJ_le_breakdownLegB {d : ℕ} {Q R : HCPolySupport.TriadicCube d} {k : ℤ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) (hR : R ∈ HCPolySupport.descendantsAtScale Q k) {e : HCPolySupport.FullBlockVec d} (he : HCPolySupport.Book.Ch02.fullBlockVecNormSq e = 1) : HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (a.coeffOn R).transpose ((frameLoadSqrt a0 e).2 + (frameLoadInvSqrt a0 e).1) ((frameLoadSqrt a0 e).1 + (frameLoadInvSqrt a0 e).2) ≤ breakdownLegB R a a0

Every a^t-leg frame value of a descendant cube is bounded by the leg.

theorem Algsuperdiff.Section3.Provider.Localization.breakdownLegA_le_of_forall_frame {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) {c : ℝ} (hc : 0 ≤ c) (h : ∀ (e : HCPolySupport.FullBlockVec d), HCPolySupport.Book.Ch02.fullBlockVecNormSq e = 1 → HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (a.coeffOn R) ((frameLoadInvSqrt a0 e).1 - (frameLoadSqrt a0 e).2) ((frameLoadSqrt a0 e).1 - (frameLoadInvSqrt a0 e).2) ≤ c) : breakdownLegA R a a0 ≤ c

A uniform bound on the a-leg frame values bounds the leg. This is the entry point through which the downstream comparator normalization converts a per-frame response estimate into an estimate on the leg.

theorem Algsuperdiff.Section3.Provider.Localization.breakdownLegB_le_of_forall_frame {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) {c : ℝ} (hc : 0 ≤ c) (h : ∀ (e : HCPolySupport.FullBlockVec d), HCPolySupport.Book.Ch02.fullBlockVecNormSq e = 1 → HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (a.coeffOn R).transpose ((frameLoadSqrt a0 e).2 + (frameLoadInvSqrt a0 e).1) ((frameLoadSqrt a0 e).1 + (frameLoadInvSqrt a0 e).2) ≤ c) : breakdownLegB R a a0 ≤ c

A uniform bound on the a^t-leg frame values bounds the leg.

theorem Algsuperdiff.Section3.Provider.Localization.breakdownLegA_le_two_mul_normalizedBlockResponseMax {d : ℕ} {Q R : HCPolySupport.TriadicCube d} {k : ℤ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) (hR : R ∈ HCPolySupport.descendantsAtScale Q k) : breakdownLegA R a a0 ≤ 2 * HCPolySupport.Book.Ch02.normalizedBlockResponseMax R a a0

The a-leg of a descendant cube is bounded by twice its normalized block response.

theorem Algsuperdiff.Section3.Provider.Localization.breakdownLegB_le_two_mul_normalizedBlockResponseMax {d : ℕ} {Q R : HCPolySupport.TriadicCube d} {k : ℤ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) (hR : R ∈ HCPolySupport.descendantsAtScale Q k) : breakdownLegB R a a0 ≤ 2 * HCPolySupport.Book.Ch02.normalizedBlockResponseMax R a a0

The a^t-leg of a descendant cube is bounded by twice its normalized block response.

theorem Algsuperdiff.Section3.Provider.Localization.normalizedBlockResponseMax_le_breakdownLegA_add_breakdownLegB {d : ℕ} {Q R : HCPolySupport.TriadicCube d} {k : ℤ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) (hR : R ∈ HCPolySupport.descendantsAtScale Q k) : HCPolySupport.Book.Ch02.normalizedBlockResponseMax R a a0 ≤ 1 / 2 * (breakdownLegA R a a0 + breakdownLegB R a a0)

The per-cube two-leg split. The block functional from which 𝓔_{s,p,q} is built is bounded by half the sum of the two scalar frame legs, because the doubled response splits unconditionally into the primal and adjoint halves with the weight 1/2 on each (Book.Ch02.doubledResponseJ_eq_half_responseJ_adjoint_sum).

The 1/2 is the arithmetic content of the splitting and is retained here: the weaker bound by the full sum — obtained by discarding each 1/2 against responseJ_nonneg — would double the constant of e.mathcal.E.breakdown against the printed display. Retaining the 1/2 uses strictly fewer inputs than discarding it: only the splitting identity and the two frame bounds responseJ_le_breakdownLegA / responseJ_le_breakdownLegB, and no nonnegativity of the individual scalar responses.

The per-scale power mean and the weighted leg sums

noncomputable def Algsuperdiff.Section3.Provider.Localization.legScaleAverage {d : ℕ} (Q : HCPolySupport.TriadicCube d) (k : ℤ) (s : ℝ) (leg : HCPolySupport.TriadicCube d → ℝ) : ℝ

The per-scale power mean of a leg at the printed exponents of e.mathcal.E.breakdown: (⨍_{z ∈ 3^k ℤ^d ∩ Q} leg(z + □_k)^{d/s})^{s/d}.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Localization.legScaleAverage_nonneg {d : ℕ} (Q : HCPolySupport.TriadicCube d) (k : ℤ) (s : ℝ) {leg : HCPolySupport.TriadicCube d → ℝ} (hleg : ∀ R ∈ HCPolySupport.descendantsAtScale Q k, 0 ≤ leg R) : 0 ≤ legScaleAverage Q k s leg

The per-scale power mean of a nonnegative leg is nonnegative.

theorem Algsuperdiff.Section3.Provider.Localization.legScaleAverage_le_const {d : ℕ} (Q : HCPolySupport.TriadicCube d) (k : ℤ) {s : ℝ} (hs : 0 < s) {leg : HCPolySupport.TriadicCube d → ℝ} {D : ℝ} (hD : 0 ≤ D) (hleg : ∀ R ∈ HCPolySupport.descendantsAtScale Q k, 0 ≤ leg R) (hle : ∀ R ∈ HCPolySupport.descendantsAtScale Q k, leg R ≤ D) (hd : d ≠ 0) : legScaleAverage Q k s leg ≤ D

A uniform bound on a nonnegative leg bounds its per-scale power mean.

theorem Algsuperdiff.Section3.Provider.Localization.legScaleAverage_smul {d : ℕ} (Q : HCPolySupport.TriadicCube d) (k : ℤ) {s : ℝ} (hs : 0 < s) (hd : d ≠ 0) {c : ℝ} (hc : 0 ≤ c) {leg : HCPolySupport.TriadicCube d → ℝ} (hleg : ∀ R ∈ HCPolySupport.descendantsAtScale Q k, 0 ≤ leg R) : (legScaleAverage Q k s fun (R : HCPolySupport.TriadicCube d) => c * leg R) = c * legScaleAverage Q k s leg

Positive homogeneity of the per-scale power mean. The power mean (⨍ leg^{d/s})^{s/d} is degree-one homogeneous in a nonnegative leg, so a nonnegative constant factor passes through it unchanged. This is what carries the 1/2 of the block splitting (normalizedBlockResponseMax_le_breakdownLegA_add_breakdownLegB) out of the per-scale average and into the constant of e.mathcal.E.breakdown.

theorem Algsuperdiff.Section3.Provider.Localization.legScaleAverage_le_add {d : ℕ} (Q : HCPolySupport.TriadicCube d) (k : ℤ) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (hd : d ≠ 0) {leg legA legB : HCPolySupport.TriadicCube d → ℝ} (hA : ∀ R ∈ HCPolySupport.descendantsAtScale Q k, 0 ≤ legA R) (hB : ∀ R ∈ HCPolySupport.descendantsAtScale Q k, 0 ≤ legB R) (hleg : ∀ R ∈ HCPolySupport.descendantsAtScale Q k, 0 ≤ leg R) (hsplit : ∀ R ∈ HCPolySupport.descendantsAtScale Q k, leg R ≤ legA R + legB R) : legScaleAverage Q k s leg ≤ legScaleAverage Q k s legA + legScaleAverage Q k s legB

Minkowski's inequality at one scale. For s ≤ 1 ≤ d the inner exponent d/s is at least one, so the per-scale power mean is subadditive in the leg.

noncomputable def Algsuperdiff.Section3.Provider.Localization.breakdownLegSum {d : ℕ} (m : ℤ) (s : ℝ) (leg : HCPolySupport.TriadicCube d → ℝ) : ℝ

The weighted leg sum of e.mathcal.E.breakdown, Σ_{l=-∞}^m 3^{-s(m-l)} (⨍_{z ∈ 3^l ℤ^d ∩ □_m} leg(z+□_l)^{d/s})^{s/d}, reindexed by the depth j = m - l ∈ ℕ.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Localization.summable_breakdownLegSum_terms {d : ℕ} [NeZero d] (m : ℤ) {s : ℝ} (hs : 0 < s) {leg : HCPolySupport.TriadicCube d → ℝ} {D : ℝ} (hD : 0 ≤ D) (hleg0 : ∀ (R : HCPolySupport.TriadicCube d), 0 ≤ leg R) (hlegle : ∀ (j : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - ↑j), leg R ≤ D) : Summable fun (j : ℕ) => Real.rpow 3 (-s * ↑j) * legScaleAverage (HCPolySupport.originCube d m) (m - ↑j) s leg

The summability producer. The leg series of the display is summable: each leg is bounded on the descendants by twice CoarseGraining's structural uniform response bound for the root cube, so the series is dominated by a convergent geometric series.

This is public because it is the intended producer of the Summable side conditions of the leg series: a consumer discharges them by supplying a uniform descendant bound D on its leg rather than by re-proving the domination argument.

theorem Algsuperdiff.Section3.Provider.Localization.homogenizationErrorOnCube_sq_le_breakdown {d : ℕ} [NeZero d] (m : ℤ) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : HCPolySupport.Book.Ch02.HomogenizationErrorOnCube (HCPolySupport.originCube d m) s HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a a0 ^ 2 ≤ 1 / 2 * (HCPolySupport.Book.Ch02.geometricDiscount s 2 * breakdownLegSum m s fun (R : HCPolySupport.TriadicCube d) => breakdownLegA R a a0) + 1 / 2 * (HCPolySupport.Book.Ch02.geometricDiscount s 2 * breakdownLegSum m s fun (R : HCPolySupport.TriadicCube d) => breakdownLegB R a a0)

e.mathcal.E.breakdown (ABK26), pathwise on CoarseGraining's literal 𝓔_{s,∞,2} carrier.

For every triadic coefficient family a, every constant comparator a0, every cube scale m and every s ∈ (0, 1],

𝓔_{s,∞,2}(□_m; a, a0)^2
  ≤ (1/2) c_{2s} Σ_{l ≤ m} 3^{-s(m-l)}
      (⨍_{z ∈ 3^l ℤ^d ∩ □_m} legA(z+□_l)^{d/s})^{s/d}
  + (1/2) c_{2s} Σ_{l ≤ m} 3^{-s(m-l)}
      (⨍_{z ∈ 3^l ℤ^d ∩ □_m} legB(z+□_l)^{d/s})^{s/d},

with legA/legB the primal and adjoint frame legs and c_{2s} = 1 - 3^{-2s} = geometricDiscount s 2.

This is the printed display verbatim. The exact accounting: legA and legB are the frame suprema over the doubled unit sphere, and at the scalar comparator each equals twice the printed max_{|e|=1} object ([P]). The per-scale power mean is degree-one homogeneous (legScaleAverage_smul), so (1/2) * breakdownLegSum m s legA is exactly the printed sum Σ_{l ≤ m} 3^{-s(m-l)} (⨍ max_{|e|=1} J(z+□_l, a0^{-1/2}e, a0^{1/2}e; a)^{d/s})^{s/d}, and likewise for legB with a^t. Under that identification the two sides of this inequality are the two sides of e.mathcal.E.breakdown with the same constant c_{2s} — the doubling of the legs and the 1/2 of the block splitting (normalizedBlockResponseMax_le_breakdownLegA_add_breakdownLegB) cancel here, rather than being asserted to cancel later.

The endpoint s = 1 is included; see the module docstring for the disclosure of the printed range of e.mathcalE.infty.to.q and of the frame-sup normalization.

The two frame combinations and their size

def Algsuperdiff.Section3.Provider.Localization.frameLegAVec {d : ℕ} (e : HCPolySupport.FullBlockVec d) : HCPolySupport.Vec d

The primal frame combination e₁ - e₂ of a doubled direction e.

Equations

• Algsuperdiff.Section3.Provider.Localization.frameLegAVec e = (HCPolySupport.ofFullBlockVec e).1 - (HCPolySupport.ofFullBlockVec e).2

def Algsuperdiff.Section3.Provider.Localization.frameLegBVec {d : ℕ} (e : HCPolySupport.FullBlockVec d) : HCPolySupport.Vec d

The adjoint frame combination e₁ + e₂ of a doubled direction e.

Equations

• Algsuperdiff.Section3.Provider.Localization.frameLegBVec e = (HCPolySupport.ofFullBlockVec e).1 + (HCPolySupport.ofFullBlockVec e).2

theorem Algsuperdiff.Section3.Provider.Localization.vecNormSq_frameLegAVec_le {d : ℕ} (e : HCPolySupport.FullBlockVec d) (he : HCPolySupport.Book.Ch02.fullBlockVecNormSq e = 1) : HCPolySupport.vecNormSq (frameLegAVec e) ≤ 2

The primal loading vector of a doubled unit direction has squared length at most 2.

theorem Algsuperdiff.Section3.Provider.Localization.vecNormSq_frameLegBVec_le {d : ℕ} (e : HCPolySupport.FullBlockVec d) (he : HCPolySupport.Book.Ch02.fullBlockVecNormSq e = 1) : HCPolySupport.vecNormSq (frameLegBVec e) ≤ 2

The adjoint loading vector of a doubled unit direction has squared length at most 2.

The isotropic comparator acts diagonally on the doubled frame

The legs in the manuscript's paired form

theorem Algsuperdiff.Section3.Provider.Localization.breakdownLegAValueSet_isotropic_eq {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (sigma : Observable.PositiveScalar) : breakdownLegAValueSet R a (Observable.isotropicComparatorMatrix sigma) = {x : ℝ | ∃ (e : HCPolySupport.FullBlockVec d), HCPolySupport.Book.Ch02.fullBlockVecNormSq e = 1 ∧ x = HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (a.coeffOn R) (Observable.inverseSqrtLoad sigma (frameLegAVec e)) (Observable.sqrtLoad sigma (frameLegAVec e))}

The primal leg at the isotropic comparator is the manuscript's paired family. Each doubled unit direction e contributes exactly J(R, σ^{-1/2}v, σ^{1/2}v; a) at the loading vector v = e₁ - e₂.

theorem Algsuperdiff.Section3.Provider.Localization.breakdownLegBValueSet_isotropic_eq {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (sigma : Observable.PositiveScalar) : breakdownLegBValueSet R a (Observable.isotropicComparatorMatrix sigma) = {x : ℝ | ∃ (e : HCPolySupport.FullBlockVec d), HCPolySupport.Book.Ch02.fullBlockVecNormSq e = 1 ∧ x = HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (a.coeffOn R).transpose (Observable.inverseSqrtLoad sigma (frameLegBVec e)) (Observable.sqrtLoad sigma (frameLegBVec e))}

The adjoint leg at the isotropic comparator is the manuscript's paired family. Each doubled unit direction e contributes exactly J(R, σ^{-1/2}v, σ^{1/2}v; a^t) at the loading vector v = e₁ + e₂.

The consumption interface

theorem Algsuperdiff.Section3.Provider.Localization.breakdownLegA_le_of_paired_bound {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (sigma : Observable.PositiveScalar) {c : ℝ} (hc : 0 ≤ c) (h : ∀ (v : HCPolySupport.Vec d), HCPolySupport.vecNormSq v ≤ 2 → HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (a.coeffOn R) (Observable.inverseSqrtLoad sigma v) (Observable.sqrtLoad sigma v) ≤ c) : breakdownLegA R a (Observable.isotropicComparatorMatrix sigma) ≤ c

The primal leg under a paired-loading bound. A bound on the manuscript's paired response J(R, σ^{-1/2}v, σ^{1/2}v; a), uniform over loading vectors of squared Euclidean length at most 2, bounds the leg. This is the interface through which the localization proof's per-cube estimates — which are proved at paired unit loadings — reach the legs of e.mathcal.E.breakdown; the excess length √2 is exactly the doubling recorded in [P].

theorem Algsuperdiff.Section3.Provider.Localization.breakdownLegB_le_of_paired_bound {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (sigma : Observable.PositiveScalar) {c : ℝ} (hc : 0 ≤ c) (h : ∀ (v : HCPolySupport.Vec d), HCPolySupport.vecNormSq v ≤ 2 → HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (a.coeffOn R).transpose (Observable.inverseSqrtLoad sigma v) (Observable.sqrtLoad sigma v) ≤ c) : breakdownLegB R a (Observable.isotropicComparatorMatrix sigma) ≤ c

The adjoint leg under a paired-loading bound.

The Section 3 carrier

theorem Algsuperdiff.Section3.Provider.Localization.neZero_of_abkModel {d : ℕ} (M : ABKModel d) : NeZero d

The paper-wide dimension assumption 2 ≤ d stored in the model discharges the [NeZero d] binder carried by the statements of this file. That binder is therefore typing data for the block carriers, not an additional mathematical premise: any caller holding an ABKModel d can supply it.

theorem Algsuperdiff.Section3.Provider.Localization.cutoffHomogenizationError_sq_ae_le_breakdown {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) (hs1 : ↑s ≤ 1) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), Observable.cutoffHomogenizationError M m s omega ^ 2 ≤ 1 / 2 * (HCPolySupport.Book.Ch02.geometricDiscount (↑s) 2 * breakdownLegSum m ↑s fun (R : HCPolySupport.TriadicCube d) => breakdownLegA R (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega) (Observable.isotropicComparatorMatrix (Annealed.sigmaBar M m))) + 1 / 2 * (HCPolySupport.Book.Ch02.geometricDiscount (↑s) 2 * breakdownLegSum m ↑s fun (R : HCPolySupport.TriadicCube d) => breakdownLegB R (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega) (Observable.isotropicComparatorMatrix (Annealed.sigmaBar M m)))

e.mathcal.E.breakdown on the Section 3 carrier (ABK26). For the measurable Section 3 observable 𝓔_{s,∞,2}(□_m; a_m, σ_m) at any s ∈ (0, 1],

𝓔_{s,∞,2}(□_m; a_m, σ_m)^2
  ≤ (1/2) c_{2s} Σ_{l ≤ m} 3^{-s(m-l)}
      (⨍_{z ∈ 3^l ℤ^d ∩ □_m} legA(z+□_l; a_m, σ_m)^{d/s})^{s/d}
  + (1/2) c_{2s} Σ_{l ≤ m} 3^{-s(m-l)}
      (⨍_{z ∈ 3^l ℤ^d ∩ □_m} legB(z+□_l; a_m, σ_m)^{d/s})^{s/d}

almost surely under the cutoff-sample law, with legA the primal and legB the adjoint frame leg at the σ_m-normalized loadings.

This is the printed display verbatim, with the same accounting as homogenizationErrorOnCube_sq_le_breakdown: each leg is twice the printed max_{|e|=1} object, the per-scale power mean is degree-one homogeneous (legScaleAverage_smul), so (1/2) * breakdownLegSum m s legA is exactly the printed sum and the constant is the printed c_{2s}.

The inequality itself is deterministic (homogenizationErrorOnCube_sq_le_breakdown); the almost-sure quantifier, and the fact that its null set sits inside the s binder, come only from the verified measurable representative underlying Observable.cutoffHomogenizationError, whose identification with CoarseGraining's literal 𝓔_{s,∞,2} is itself indexed by s ([F]).