Cross-pairing complement core estimates at order two

The difference-retaining estimate reduces the order-two middle estimate to the complement schedules: contractions whose within-half pairings are trivial (idPairingFinTwo in both halves), so that no primitive interval is extracted, no difference factor exists, and the two halves are coupled only through the two cross-half covariance factors — the paper §4.2 Step 3 cross-cut objects.

This file proves the scalar analytic core:

• integral_charT4_mul_etaEpsT4_shift — the exact translated covariance mode: ∫ charT4 b s · η_ε(v-s) = charT4 b v · (2π)⁴ ĉ(b);
• integral_integral_charT4_greenFn_pair — the two-variable Green–character orthogonality ∫∫ G(s-t) e_a(s) e_b(t) = (2π)⁴ ⟨b⟩⁻² [a+b=0];
• integral_pi_crossHalf_eq_tsum — the coupled half collapse: the half chain integrated against both cross covariances is the explicit diagonal mode series;
• integral_crossCore_le_tsum — the full cross-cut core ∫∫ G G η η = Σ_k ĉ(k)² ⟨k⟩⁻⁴-type diagonal window, bounded by Σ_k ‖ρ̂(εk)‖⁴ ⟨k⟩⁻⁴;
• exists_crossWindow_le_log — the ε-supported window sum is ≤ C(ρ)·|log ε|: the low cube |k|∞ ≤ ⌈ε⁻¹⌉ contributes the harmonic-shell logarithm, and the tail is O(1) by the degree-8 Schwartz decay of the mollifier symbol against the eighth-order radial tail.

The constant is uniform in ε, λ, and both external modes, but (in contrast with the difference-retaining two-block bound) genuinely depends on the mollifier: as the mollifier radius shrinks, the symbol window widens to |k| ≲ (radius·ε)⁻¹ and the diagonal sum grows like |log ε| + |log radius|.

Character algebra on differences

theorem Anderson4D.charT4_mul_charT4_neg_self (k : Z4) (x : T4) : charT4 k x * charT4 (-k) x = 1

theorem Anderson4D.charT4_sub (k : Z4) (x y : T4) : charT4 k (x - y) = charT4 k x * charT4 (-k) y

Characters split across a difference of points.

theorem Anderson4D.paperModeNormSq_neg (k : Z4) : paperModeNormSq (-k) = paperModeNormSq k

The exact translated covariance mode

theorem Anderson4D.integrable_charT4 (k : Z4) : MeasureTheory.Integrable (charT4 k) paperMeasure

theorem Anderson4D.integral_charT4_mul_etaEpsT4_shift (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (b : Z4) (v : T4) : ∫ (s : T4), charT4 b s * ↑(ρ.etaEpsT4 ε (v - s)) ∂paperMeasure = charT4 b v * (↑((2 * Real.pi) ^ dim) * ρ.covarianceModeCoeff ε b)

The translated covariance mode, exactly. Integrating one character against a translated covariance extracts the base-point character times the total-mass-normalized Fourier coefficient.

Two-variable Green--character orthogonality

theorem Anderson4D.integrable_greenFn_pair : MeasureTheory.Integrable (fun (p : T4 × T4) => greenFn (p.1 - p.2)) (paperMeasure.prod paperMeasure)

The Green pair kernel is integrable on the product.

theorem Anderson4D.integral_integral_charT4_greenFn_pair (a b : Z4) : ∫ (s : T4), ∫ (t : T4), charT4 a s * charT4 b t * ↑(greenFn (s - t)) ∂paperMeasure ∂paperMeasure = if a + b = 0 then ↑((2 * Real.pi) ^ dim * (1 + paperModeNormSq b)⁻¹) else 0

Two-variable Green--character orthogonality. The double integral of the Green edge against two characters is diagonal: it vanishes unless the two modes cancel, and then carries one boundary coefficient and one paper volume.

Translated covariance mass

theorem Anderson4D.integrable_etaEpsT4_sub (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (z : T4) : MeasureTheory.Integrable (fun (x : T4) => ρ.etaEpsT4 ε (x - z)) paperMeasure

theorem Anderson4D.integral_etaEpsT4_sub_le_one (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (z : T4) : ∫ (x : T4), ρ.etaEpsT4 ε (x - z) ∂paperMeasure ≤ 1

The coupled cross-half collapse

noncomputable def Anderson4D.r324CrossPairCoefficient (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : ℂ

The diagonal coefficient of one cross-cut covariance pairing: one boundary Green weight, one paper volume, and the squared covariance mode.

Equations

• Anderson4D.r324CrossPairCoefficient ρ ε k = ↑(1 + Anderson4D.paperModeNormSq k)⁻¹ * ↑((2 * Real.pi) ^ Anderson4D.dim) * ρ.covarianceModeCoeff ε k ^ 2

theorem Anderson4D.integral_integral_greenFn_etaPair_eq_tsum (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (p q : T4) : ∫ (t : T4), ∫ (s : T4), ↑(greenFn (s - t) * (ρ.etaEpsT4 ε (s - p) * ρ.etaEpsT4 ε (t - q))) ∂paperMeasure ∂paperMeasure = ∑' (k : Z4), r324CrossPairCoefficient ρ ε k * (charT4 (-k) p * charT4 k q)

The coupled half collapses to a diagonal mode series. The half chain edge is integrated jointly with both cross covariances; the two internal integrals produce one Green coefficient and one squared covariance coefficient on the same mode, tied to the two coupling points by opposite characters.

The outer cross-cut collapse

theorem Anderson4D.integral_prod_greenFn : ∫ (r : T4 × T4), greenFn (r.1 - r.2) ∂paperMeasure.prod paperMeasure = (2 * Real.pi) ^ dim

theorem Anderson4D.integral_prod_charPair_greenFn (a b : Z4) : ∫ (r : T4 × T4), charT4 a r.1 * charT4 b r.2 * ↑(greenFn (r.1 - r.2)) ∂paperMeasure.prod paperMeasure = if a + b = 0 then ↑((2 * Real.pi) ^ dim * (1 + paperModeNormSq b)⁻¹) else 0

Product form of the two-variable Green--character orthogonality.

theorem Anderson4D.norm_r324CrossPairCoefficient_le (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : ‖r324CrossPairCoefficient ρ ε k‖ ≤ ‖ρ.covarianceModeCoeff ε k‖

theorem Anderson4D.integral_prod_greenFn_mul_tsum_crossModes (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (a b : Z4 → Z4) (hab : ∀ (k : Z4), a k + b k = 0) (hbP : ∀ (k : Z4), paperModeNormSq (b k) = paperModeNormSq k) : ∫ (r : T4 × T4), ↑(greenFn (r.1 - r.2)) * ∑' (k : Z4), r324CrossPairCoefficient ρ ε k * (charT4 (a k) r.1 * charT4 (b k) r.2) ∂paperMeasure.prod paperMeasure = ∑' (k : Z4), r324CrossPairCoefficient ρ ε k * ↑((2 * Real.pi) ^ dim * (1 + paperModeNormSq k)⁻¹)

The outer cross-cut collapse. The second half chain edge integrated against the diagonal mode series of the collapsed first half: every mode pairs its opposite characters across the outer edge and receives the second boundary Green coefficient. The two possible cross matchings differ only in the character arrangement, absorbed by the hypotheses.

The ε-supported diagonal window

theorem Anderson4D.paperModeNormSq_eq_and_supRadius_le (k : Z4) : ↑(z4SupRadius k) ^ 2 ≤ paperModeNormSq k

theorem Anderson4D.inv_one_add_paperModeNormSq_le (k : Z4) : (1 + paperModeNormSq k)⁻¹ ≤ 2 * ((1 + ↑(z4SupRadius k)) ^ 2)⁻¹

The Euclidean bracket dominated by the sup bracket: (1+P)⁻¹ ≤ 2 (1+s)⁻².

theorem Anderson4D.symbol_sq_le_of_decay (ρ : SmoothCutoff) {C0 : ℝ} (hdecay : ∀ (ξ : R4), (1 + ‖SmoothCutoff.euclideanFrequency ξ‖) ^ 8 * ‖fourierR4 ρ.toFun ξ‖ ≤ C0) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (k : Z4) : ‖ρ.symbol ε k‖ ^ 2 ≤ C0 ^ 2 * (2 * Real.pi) ^ 4 * (ε⁻¹ ^ 4 * ((1 + ↑(z4SupRadius k)) ^ 4)⁻¹)

Degree-two decay of the scaled symbol against the sup bracket, uniformly in the scale: ‖ρ̂(εk)‖ ≤ 2π C₀ ε⁻¹ (1+s)⁻¹-squared form.

theorem Anderson4D.exists_crossWindow_le_log (ρ : SmoothCutoff) : ∃ (CW : ℝ), 0 < CW ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → ∑' (k : Z4), ‖ρ.symbol ε k‖ ^ 4 * (1 + paperModeNormSq k)⁻¹ ^ 2 ≤ CW * |Real.log ε|

The ε-supported diagonal window is logarithmic. Inside the cube |k|∞ ≤ ⌈ε⁻¹⌉ the unit symbol bound leaves the fourth-order shell sum ≈ log; outside, the degree-8 Schwartz decay of the symbol converts four inverse powers of ε into the eighth-order radial tail ≤ 20 (N+1)⁻⁴ ≤ 20 ε⁴. The constant depends only on the mollifier.

The trivial-pairing half integrand

theorem Anderson4D.idPairingFinTwo_extract : extract idPairingFinTwo = []

theorem Anderson4D.detIntegrand_idPairingFinTwo_assemble (ρ : SmoothCutoff) (ε : ℝ) (x y : T4) (u : Fin 2 → T4) : detIntegrand ρ ε 2 idPairingFinTwo (assemble x y u) = greenFn (x - u 0) * greenFn (u 0 - u 1) * greenFn (u 1 - y)

Closed form of the order-two trivial-pairing integrand: the plain three-edge chain. Nothing is extracted, no difference factor exists, and no within-half covariance appears.

The two cross matchings

def Anderson4D.idSingleZero : ↥idPairingFinTwo.singles

The first single of the trivial pairing.

Equations

• Anderson4D.idSingleZero = ⟨0, Anderson4D.idSingleZero._proof_1⟩

def Anderson4D.idSingleOne : ↥idPairingFinTwo.singles

The second single of the trivial pairing.

Equations

• Anderson4D.idSingleOne = ⟨1, Anderson4D.idSingleOne._proof_1⟩

theorem Anderson4D.idSingle_cases (j : ↥idPairingFinTwo.singles) : j = idSingleZero ∨ j = idSingleOne

theorem Anderson4D.crossSingleEquiv_classify (π : ↥idPairingFinTwo.singles ≃ ↥idPairingFinTwo.singles) : π idSingleZero = idSingleZero ∧ π idSingleOne = idSingleOne ∨ π idSingleZero = idSingleOne ∧ π idSingleOne = idSingleZero

A bijection of the trivial singles is the identity matching or the swap matching.

theorem Anderson4D.momentCrossCovarianceProduct_id_id (ρ : SmoothCutoff) (ε : ℝ) (π : ↥idPairingFinTwo.singles ≃ ↥idPairingFinTwo.singles) (v : Fin (2 * 2) → T4) : momentCrossCovarianceProduct ρ ε 2 idPairingFinTwo idPairingFinTwo π v = ρ.etaEpsT4 ε (v (leftMomentIndex 0) - v (rightMomentIndex ↑(π idSingleZero))) * ρ.etaEpsT4 ε (v (leftMomentIndex 1) - v (rightMomentIndex ↑(π idSingleOne)))

The cross covariance of a trivial-pairing contraction: exactly the two cross-half factors selected by the matching.

The cross physical density and its exact external peeling

noncomputable def Anderson4D.r324CrossCoreDensity (ρ : SmoothCutoff) (ε : ℝ) (j₀ j₁ : Fin 2) (v : Fin (2 * 2) → T4) : ℝ

The internal core of the cross density: both middle chain edges against both cross covariances.

Equations

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

noncomputable def Anderson4D.r324CrossPhysicalDensity (ρ : SmoothCutoff) (ε : ℝ) (j₀ j₁ : Fin 2) (p : R324PhysicalPoint 2) : ℝ

The full cross physical density in peel-ready nested form: each external variable multiplies one unit-mass boundary Green edge.

Equations

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

theorem Anderson4D.integral_flat_crossPhysicalDensity (ρ : SmoothCutoff) (ε : ℝ) (j₀ j₁ : Fin 2) (hint : MeasureTheory.Integrable (r324CrossPhysicalDensity ρ ε j₀ j₁) (r324PhysicalMeasure 2)) : ∫ (p : R324PhysicalPoint 2), r324CrossPhysicalDensity ρ ε j₀ j₁ p ∂r324PhysicalMeasure 2 = ∫ (v : Fin (2 * 2) → T4), r324CrossCoreDensity ρ ε j₀ j₁ v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * 2)) => paperMeasure

Exact peeling of the four external variables. Each boundary Green edge has unit paper mass; the flat cross density integrates to the internal core integral.

The internal core evaluation

theorem Anderson4D.integrable_crossHalfPair (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (p q : T4) : MeasureTheory.Integrable (fun (r : T4 × T4) => ↑(greenFn (r.1 - r.2) * (ρ.etaEpsT4 ε (r.1 - p) * ρ.etaEpsT4 ε (r.2 - q)))) (paperMeasure.prod paperMeasure)

theorem Anderson4D.norm_crossPairMode_eq (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : ‖r324CrossPairCoefficient ρ ε k * ↑((2 * Real.pi) ^ dim * (1 + paperModeNormSq k)⁻¹)‖ = ‖ρ.symbol ε k‖ ^ 4 * (1 + paperModeNormSq k)⁻¹ ^ 2

theorem Anderson4D.summable_crossWindowTerm (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : Summable fun (k : Z4) => ‖ρ.symbol ε k‖ ^ 4 * (1 + paperModeNormSq k)⁻¹ ^ 2

theorem Anderson4D.integral_crossCoreDensity_le (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {j₀ j₁ : Fin 2} (hj : j₀ = 0 ∧ j₁ = 1 ∨ j₀ = 1 ∧ j₁ = 0) (hint : MeasureTheory.Integrable (r324CrossCoreDensity ρ ε j₀ j₁) (MeasureTheory.Measure.pi fun (x : Fin (2 * 2)) => paperMeasure)) : (∫ (v : Fin (2 * 2) → T4), r324CrossCoreDensity ρ ε j₀ j₁ v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * 2)) => paperMeasure) ≤ ∑' (k : Z4), ‖ρ.symbol ε k‖ ^ 4 * (1 + paperModeNormSq k)⁻¹ ^ 2

The internal cross core is the diagonal window. Both middle chain edges integrated against both cross covariances collapse, for either matching, to the diagonal mode sum Σ_k ‖ρ̂(εk)‖⁴ ⟨k⟩⁻⁴-type — the squared-Green analogue of the raw block mass, with no ε-divergence.

theorem Anderson4D.integrable_crossCoreDensity_of_flat (ρ : SmoothCutoff) (ε : ℝ) (j₀ j₁ : Fin 2) (hint : MeasureTheory.Integrable (r324CrossPhysicalDensity ρ ε j₀ j₁) (r324PhysicalMeasure 2)) : MeasureTheory.Integrable (r324CrossCoreDensity ρ ε j₀ j₁) (MeasureTheory.Measure.pi fun (x : Fin (2 * 2)) => paperMeasure)

The internal core inherits integrability from the flat density through the same four unit-mass peels.

theorem Anderson4D.norm_deterministicMomentContractionTerm_cross_le (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (α β : Z4) (π : ↥idPairingFinTwo.singles ≃ ↥idPairingFinTwo.singles) : ‖deterministicMomentContractionTerm ρ ε 2 α β ⟨idPairingFinTwo, ⟨idPairingFinTwo, π⟩⟩‖ ≤ ∑' (k : Z4), ‖ρ.symbol ε k‖ ^ 4 * (1 + paperModeNormSq k)⁻¹ ^ 2

The cross contraction term obeys the diagonal window bound. For either cross matching, the complete order-two trivial-pairing contraction term is bounded by the diagonal mode window — with all four external variables consumed at unit mass and no dependence on the external modes.

theorem Anderson4D.exists_norm_crossContractionTerm_le_log (ρ : SmoothCutoff) : ∃ (CW : ℝ), 0 < CW ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → ∀ (α β : Z4) (π : ↥idPairingFinTwo.singles ≃ ↥idPairingFinTwo.singles), ‖deterministicMomentContractionTerm ρ ε 2 α β ⟨idPairingFinTwo, ⟨idPairingFinTwo, π⟩⟩‖ ≤ CW * |Real.log ε|

Logarithmic bound for the cross contraction term. The mollifier-dependent constant is uniform in the scale, the coupling, and both external modes.