Difference-retaining block estimates for R-324

The order-two interior-core budget fails by not_r324InteriorCoreLogBudget_two: the terminal swap block must be integrated jointly with its renormalizing difference factor G(v₁-y) - G(v₀-y) before any endpoint sup-normalization.

This file proves the scalar ledger of that joint integration:

• exists_integral_torusDistSq_mul_greenFn_mul_etaEpsT4_le — the second-moment mass ∫ |z̃|² G η_ε of the block pair coordinate is bounded by a constant uniform in ρ and ε: the quadratic weight exactly cancels the Green singularity (G ≤ C|z̃|⁻²), leaving only the unit covariance mass ∫ η_ε ≤ 1;
• norm_r324BlockFrequencyIntegral_le — the renormalized block frequency integral M(β) = ∫ G η_ε (e^{iβ·z} - 1) obeys the second-order bound |M(β)| ≤ (1/2)|β|² ∫ |z̃|² G η_ε: the first-order term is killed by the parity of G η_ε (cosine seam), and the remaining cosine defect is quadratic. Thus the raw block mass ∫ G η_ε ≈ ε⁻² is replaced by the ε-uniform bound O(‖β‖²);
• detIntegrand_pairingFinTwo_assemble, integral_charT4_mul_detIntegrand_pairingFinTwo, integral_greenFn_mul_etaEpsT4_mul_charDiff, integral_pi_twoBlock_u — exact joint evaluation of the two-block half: the difference factor is consumed with the block before any boundary normalization;
• norm_r324TwoBlockHalfIntegral_le — one half of the two-block physical integral is bounded by (2π)⁴ (1+|β|²)⁻¹ ‖M(β)‖, uniformly in ε and both modes.

The physical integrand detIntegrand (paper (3.6)) retains every extracted diffFactor; the endpoint-first majorant loses the terminal chain edge when r324RefinedInteriorCore separates the sup-normalized endpoint legs. The estimate is therefore proved at the level of r324RefinedPhysicalIntegral, before the interior/endpoint split.

The quadratic block mass is ε-uniform

theorem Anderson4D.SmoothCutoff.integrable_etaEpsT4_paper (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : MeasureTheory.Integrable (ρ.etaEpsT4 ε) paperMeasure

The periodized covariance is integrable: it is measurable, bounded (uniformly at fixed scale), and the paper measure is finite.

theorem Anderson4D.integrable_torusDistSq_mul_greenFn_mul_etaEpsT4 (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : MeasureTheory.Integrable (fun (z : T4) => torusDistSq z * (greenFn z * ρ.etaEpsT4 ε z)) paperMeasure

The quadratically weighted Green--covariance block mass, with its integrability.

theorem Anderson4D.exists_integral_torusDistSq_mul_greenFn_mul_etaEpsT4_le : ∃ (K : ℝ), 0 < K ∧ ∀ (ρ : SmoothCutoff) {ε : ℝ}, 0 < ε → ε ≤ 1 → ∫ (z : T4), torusDistSq z * (greenFn z * ρ.etaEpsT4 ε z) ∂paperMeasure ≤ K

ε-uniform quadratic block mass. The weight |z̃|² cancels the Green singularity exactly, so only the unit covariance mass survives: ∫ |z̃|² G η_ε ≤ C, with C independent of the cutoff and of the scale.

The renormalized block frequency integral

noncomputable def Anderson4D.r324BlockFrequencyIntegral (ρ : SmoothCutoff) (ε : ℝ) (b : Z4) : ℂ

The joint (difference-retained) block frequency integral: the Green--covariance pair against the renormalizing phase defect.

Equations

• Anderson4D.r324BlockFrequencyIntegral ρ ε b = ∫ (z : Anderson4D.T4), ↑(Anderson4D.greenFn z * ρ.etaEpsT4 ε z) * (Anderson4D.charT4 b z - 1) ∂Anderson4D.paperMeasure

theorem Anderson4D.norm_r324BlockFrequencyIntegral_le (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (b : Z4) : ‖r324BlockFrequencyIntegral ρ ε b‖ ≤ 1 / 2 * paperModeNormSq b * ∫ (z : T4), torusDistSq z * (greenFn z * ρ.etaEpsT4 ε z) ∂paperMeasure

Second-order bound for the renormalized block. Parity of G η_ε kills the first-order phase term (cosine seam), and the cosine defect is quadratic; the result is ε-uniform up to the quadratic mass, in stark contrast with the raw block mass ∫ G η_ε ≥ c ε⁻² of exists_le_integral_greenFn_mul_etaEpsT4.

The two-block renormalized integrand, closed form

theorem Anderson4D.charT4_point_add (k : Z4) (x z : T4) : charT4 k (x + z) = charT4 k x * charT4 k z

Characters are multiplicative in the point variable.

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

Closed form of the order-two renormalized swap integrand. The extraction of the unique within-half pair erases the terminal chain edge and installs the renormalizing difference factor G(u₁-y) - G(u₀-y) in its place; the covariance factor pairs the two internal vertices.

Exact one-variable evaluations

theorem Anderson4D.integrable_charT4_mul_greenFn_sub (b : Z4) (z : T4) : MeasureTheory.Integrable (fun (y : T4) => charT4 b y * ↑(greenFn (y - z))) paperMeasure

Characters against a translated Green factor are integrable.

theorem Anderson4D.integral_charT4_mul_greenFn_shift (b : Z4) (v : T4) : ∫ (y : T4), charT4 b y * ↑(greenFn (v - y)) ∂paperMeasure = charT4 b v * ↑(1 + paperModeNormSq b)⁻¹

The y-integral of one boundary Green factor with its character: the exact translated Fourier coefficient, in the orientation produced by the difference factor.

theorem Anderson4D.integral_greenFn_shift_left (x : T4) : ∫ (u : T4), greenFn (x - u) ∂paperMeasure = 1

Every left-translate of the Green kernel has unit paper mass.

theorem Anderson4D.integral_greenFn_mul_etaEpsT4_mul_charDiff (ρ : SmoothCutoff) (ε : ℝ) (b : Z4) (u₀ : T4) : ∫ (u₁ : T4), ↑(greenFn (u₀ - u₁) * ρ.etaEpsT4 ε (u₀ - u₁)) * (charT4 b u₁ - charT4 b u₀) ∂paperMeasure = charT4 b u₀ * r324BlockFrequencyIntegral ρ ε b

Joint block evaluation. Integrating the block pair coordinate against its character difference produces exactly the base-point character times the renormalized block frequency integral: the difference factor is consumed jointly with the block, never sup-normalized away.

theorem Anderson4D.integral_charT4_mul_detIntegrand_pairingFinTwo (ρ : SmoothCutoff) (ε : ℝ) (b : Z4) (x : T4) (u : Fin 2 → T4) : ∫ (y : T4), charT4 b y * ↑(detIntegrand ρ ε 2 pairingFinTwo (assemble x y u)) ∂paperMeasure = ↑(greenFn (x - u 0) * greenFn (u 0 - u 1) * ρ.etaEpsT4 ε (u 0 - u 1)) * (↑(1 + paperModeNormSq b)⁻¹ * (charT4 b (u 1) - charT4 b (u 0)))

Exact y-integral of the two-block integrand. The external character integrates the difference factor jointly with the block: the result carries the boundary Fourier coefficient (1 + |b|²)⁻¹ and the internal character difference charT4 b u₁ - charT4 b u₀, the physical-side trace of the retained renormalization.

theorem Anderson4D.norm_integral_greenFn_shift_mul_charT4_le (b : Z4) (x : T4) : ‖∫ (u₀ : T4), ↑(greenFn (x - u₀)) * charT4 b u₀ ∂paperMeasure‖ ≤ 1

The character-weighted Green translate has integral of norm at most one: the boundary leg costs exactly its unit mass.

theorem Anderson4D.integral_pi_twoBlock_u (ρ : SmoothCutoff) (ε : ℝ) (b : Z4) (x : T4) (hint : MeasureTheory.Integrable (fun (u : Fin 2 → T4) => ↑(greenFn (x - u 0) * greenFn (u 0 - u 1) * ρ.etaEpsT4 ε (u 0 - u 1)) * (↑(1 + paperModeNormSq b)⁻¹ * (charT4 b (u 1) - charT4 b (u 0)))) (MeasureTheory.Measure.pi fun (x : Fin 2) => paperMeasure)) : (∫ (u : Fin 2 → T4), ↑(greenFn (x - u 0) * greenFn (u 0 - u 1) * ρ.etaEpsT4 ε (u 0 - u 1)) * (↑(1 + paperModeNormSq b)⁻¹ * (charT4 b (u 1) - charT4 b (u 0))) ∂MeasureTheory.Measure.pi fun (x : Fin 2) => paperMeasure) = ↑(1 + paperModeNormSq b)⁻¹ * (r324BlockFrequencyIntegral ρ ε b * ∫ (u₀ : T4), ↑(greenFn (x - u₀)) * charT4 b u₀ ∂paperMeasure)

Exact evaluation of the two-block internal integral. With the difference factor consumed jointly (previous lemmas), the full internal double integral collapses to the boundary coefficient times the renormalized block frequency integral times one unit-mass boundary leg.

The two-block half integral

noncomputable def Anderson4D.r324TwoBlockHalfIntegral (ρ : SmoothCutoff) (ε : ℝ) (a b : Z4) : ℂ

One complete half of the two-block physical integral, on its flat product space: external characters against the renormalized swap integrand.

Equations

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

theorem Anderson4D.integrable_r324TwoBlockHalfIntegrand (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (a b : Z4) : MeasureTheory.Integrable (fun (p : T4 × T4 × (Fin 2 → T4)) => charT4 a p.1 * charT4 b p.2.1 * ↑(detIntegrand ρ ε 2 pairingFinTwo (assemble p.1 p.2.1 p.2.2))) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin 2) => paperMeasure)))

theorem Anderson4D.norm_r324TwoBlockHalfIntegral_le (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (a b : Z4) : ‖r324TwoBlockHalfIntegral ρ ε a b‖ ≤ (2 * Real.pi) ^ dim * ((1 + paperModeNormSq b)⁻¹ * ‖r324BlockFrequencyIntegral ρ ε b‖)

The difference-retaining half-integral bound. Uniformly in the scale and in both external frequencies, one half of the two-block physical integral is controlled by the boundary coefficient (1+|b|²)⁻¹ times the renormalized block frequency integral: the ε → 0 divergence of the raw block never appears.