VarianceSplit #

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

The variance split of Step 1 of the corrected combine proposition #

ABK26. Step 1 of p.combine.under.S leaves the two deterministic field blocks of the good-event display (CombineGoodEvent.exists_cutoffGoodEvent_cutoffResponseJ_le_preVarianceSplitDisplay)

σ_L · ⨍_{R} |σ_*^{-1}(□_m)(q + κ(□_m)p) - σ_*^{-1}(R)(q + κ(R)p)|² and
σ_L · |σ_*^{-1}(□_m)(q + κ(□_m)p) - p|²,

and converts them into the two variance blocks of e.initial.JL.bound. This module carries the deterministic and the annealed halves of that conversion, on the proved carriers.

What is proved #

The block reading of the comparison vector. The Provider.Besov.Carriers vector coarseScaleSeparation is the lower half of the coarse block matrix 𝐀(Q;a) at the block load (-p, q), minus p. The sign is forced by 𝐀_{lowerLeft} = -(σ_*^{-1}κ) (Ch02.blockMatrixOfCoarseMatrices). This gives an ellipticity-witness-free carrier coarseBlockScaleSeparation, which is what can be integrated against a coefficient law.
The two-term load split. With the Euclidean matrix operator norm -- the manuscript's |A| of -- the coarse-matrix variation is at most 2|q|²|Δσ_*^{-1}|² + 2|p|²|Δ(σ_*^{-1}κ)|².
The three-term deterministic-centering split and the printed constant 6 = 2·3.
The annealed half. (The carrier law bundles no integrability and Lean's Bochner ∫ of a non-integrable integrand is 0, so the identity "centering = mean" is honest exactly where the entries are integrable — the same scope in which the manuscript's var[·] is defined.) Real-translation stationarity collapses the printed ⨍_{z ∈ 3ⁿℤᵈ ∩ □_m} onto the single origin cube at scale n, and the result is the printed display `6|q|²(var[σ_^{-1}(□m)] + var[σ^{-1}(□n)] + |σ^{-1}(□m) - σ^{-1}(□_n)|²)
- 6|p|²(var[σ_^{-1}κ(□m)] + var[σ^{-1}κ(□_n)]). The κmean gap is *absent* rather than dropped:e.annealed.khom.zero(proved as `Provider.Annealed.coefficientCutoffLaw_annealedBlockMatrix_lowerLeft_eq_zero`) makes both annealed lower-left blocks vanish.
The e.pq.normed weights. At the manuscript loads p = σ_L^{-1/2}e, q = σ_L^{1/2}e with |e|² = 1 one has |q|² = σ_L and |p|² = σ_L^{-1}, so multiplying by the display's prefactor σ_L produces exactly the σ_L² weight on the σ_*^{-1} variances and the weight 1 on the σ_*^{-1}κ variances of e.initial.JL.bound.
Sample measurability of both good-event observables at the genuine cutoff sample law, and the reduction of their IntegrableOn over the good event to one a.e. bound.

What is NOT proved here (reported, not bound) #

The printed sandwich σ_{L,*}^{-1}(□_m) ≤ 2 σ_L^{-1} is not used anywhere below and is not supplied here; nothing in this file needs it.
The third block (vecNormSq (coarseScaleSeparation ...)) is converted here only up to the deterministic residual (σ_L σ_{L,*}^{-1}(□_m) - 1)². The residual is bounded by 4 δ₁² by combining the proved Step-2 downscale bound (coefficientCutoffLaw_sq_abs_annealedSigmaStarInvScalarAtScale_sub_le, CombineIntegerDownscale.lean) with the n → ∞ limit supplied by Annealed.sigmaBar_characterization (Annealed/RunningDiffusivity/Characterization.lean); that anchor lemma is not in this file. The printed closure, which cites only the sandwich σ_{L,*}(□_m) ≤ σ_L ≤ 2 σ_{L,*}(□_m), does not close the residual —. The residual is displayed explicitly, never bound.
The corridor sum over L ≤ n ≤ m, the reabsorption of 1/2 E[J(□_m)], and the passage from E[1_G · X] to E[X] are not performed here; the last needs integrability of the two observables on the whole space, not only on G.
The two IntegrableOn clauses are reduced to a single a.e. bound over the good event; no proved statement produces that bound. The clause is a conditional A obligation in the convention of VarianceBridge.lean and of the integrated form of VarianceCarrierSeam.lean.

This module makes no source-node status claim; every declaration is a local Provider result.

VarianceSplit #

The variance split of Step 1 of the corrected combine proposition #

What is proved #

What is NOT proved here (reported, not bound) #

Main results #

Elementary matrix and vector helpers #

The block reading of the comparison vector #

The two-term load split #

The variance carriers at the genuine cutoff law #

Stationary collapse of the printed ⨍_z #

The annealed variance display #

The e.pq.normed weights #

Sample measurability and the integrability report #

Stationary collapse of the printed `⨍_z` #

The `e.pq.normed` weights #