Base case of the deterministic interval reduction

At order 2q = 2 the non-splitting class contains only the swap pairing. Its extraction list is the whole interval, whose terminal difference factor is the value 1. This file computes that branch exactly and identifies it with the first primitive kernel.

theorem Anderson4D.pairingFinTwo_extract : extract pairingFinTwo = [(0, 1)]

theorem Anderson4D.nonSplitPairings_one_eq : nonSplitPairings 1 = {pairingFinTwo}

theorem Anderson4D.detJintegrand_one_pairingFinTwo (ρ : SmoothCutoff) (ε : ℝ) (x : Fin 2 → T4) : detJintegrand ρ ε 1 pairingFinTwo x = greenFn (x 0 - x 1) * ρ.etaEpsT4 ε (x 0 - x 1)

theorem Anderson4D.detJ_one_pairingFinTwo (ρ : SmoothCutoff) (lam ε : ℝ) (z w : T4) : detJ ρ lam ε 1 pairingFinTwo z w = lamEps lam ε ^ 2 * (greenFn (z - w) * ρ.etaEpsT4 ε (z - w))

Exact order-two J formula.

theorem Anderson4D.detJ_one_eq_primitiveKernel (ρ : SmoothCutoff) (lam ε : ℝ) (z w : T4) : detJ ρ lam ε 1 pairingFinTwo z w = primitiveKernel ρ lam ε 1 ⋯ (fun (x : Fin (2 * 1 - 1)) => greenFn) z w

The order-two deterministic kernel is literally the first primitive kernel with the free Green function as its unique chain input.

theorem Anderson4D.sum_nonSplit_detJ_abs_one (ρ : SmoothCutoff) (lam ε : ℝ) (z w : T4) : ∑ σ ∈ nonSplitPairings 1, |detJ ρ lam ε 1 σ z w| = |primitiveKernel ρ lam ε 1 ⋯ (fun (x : Fin (2 * 1 - 1)) => greenFn) z w|

theorem Anderson4D.groupedDetJAbsSum_one (ρ : SmoothCutoff) (lam ε : ℝ) (z : T4) : groupedDetJAbsSum ρ lam ε 1 z = |primitiveKernel ρ lam ε 1 ⋯ (fun (x : Fin (2 * 1 - 1)) => greenFn) z 0|

At the base order there is one endpoint signature and its fiber has one pairing, so the grouped form of (4.15) is the same single kernel.

theorem Anderson4D.renormC2q_one (ρ : SmoothCutoff) (lam ε : ℝ) : renormC2q ρ lam ε 1 = ∫ (z : T4), primitiveKernel ρ lam ε 1 ⋯ (fun (x : Fin (2 * 1 - 1)) => greenFn) z 0 ∂paperMeasure

Honest integrability of the base branch

theorem Anderson4D.SmoothCutoff.measurable_etaPeriodTerm (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : Measurable fun (z : T4) => ρ.etaPeriodTerm ε z k

theorem Anderson4D.SmoothCutoff.measurable_etaEpsT4_of_pos_of_le_one (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : Measurable (ρ.etaEpsT4 ε)

In the positive small-scale regime, the covariance periodization is a finite measurable sum. This public lemma is also useful to the later R-322 interval-integration steps.

theorem Anderson4D.integrable_detJ_one_pairingFinTwo (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : MeasureTheory.Integrable (fun (z : T4) => detJ ρ lam ε 1 pairingFinTwo z 0) paperMeasure

The exact order-two deterministic summand is genuinely integrable; this rules out any use of the junk value of the Bochner integral in the base case of R-322.

theorem Anderson4D.integrable_abs_detJ_one_pairingFinTwo (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : MeasureTheory.Integrable (fun (z : T4) => |detJ ρ lam ε 1 pairingFinTwo z 0|) paperMeasure

Absolute integrability of the base summand, derived from genuine integrability rather than used as a proxy for measurability.

Pointwise base reduction

theorem Anderson4D.eps_sq_mul_abs_log_le_one {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : ε ^ 2 * |Real.log ε| ≤ 1

theorem Anderson4D.abs_detJ_one_pairingFinTwo_le_majorant (ρ : SmoothCutoff) {Cg Cη supportConstant C lam ε : ℝ} (hCg : 0 ≤ Cg) (_hCη : 0 ≤ Cη) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 0 < |Real.log ε|) (hgreen : ∀ (z : T4), torusDistSq z ≠ 0 → greenFn z ≤ Cg / torusDistSq z) (heta : ∀ (z : T4), ρ.etaEpsT4 ε z ≤ ε⁻¹ ^ dim * Cη) (hsupport : 4 * ρ.radius ≤ supportConstant) (hClocal : Cg * Cη ≤ C ^ 2) (hCzero : greenFn 0 * Cη ≤ C ^ 2) (z : T4) : |detJ ρ lam ε 1 pairingFinTwo z 0| ≤ primitiveKernelMajorant C lam ε supportConstant 1 z

The exact base summand obeys the Proposition 4.1 majorant after absorbing the fixed Green and covariance constants. At the single singular point z = 0, the global regularized term pays for the junk-totalized value of greenFn 0; away from zero, the local |z|⁻² term is used.

theorem Anderson4D.exists_renormReductionOutput_one (ρ : SmoothCutoff) : ∃ (primitiveConstant : ℝ) (supportConstant : ℝ), 0 < primitiveConstant ∧ 0 < supportConstant ∧ ∀ (lam ε : ℝ), 0 ≤ lam → 0 < ε → ε ≤ 1 → 0 < |Real.log ε| → RenormReductionOutput ρ lam ε 1 primitiveConstant supportConstant

Fully closed R-322 output at the base perturbative order. All constants are selected before λ and ε, and both the pointwise majorant and the required integrability are proved from the concrete J kernel.

theorem Anderson4D.exists_renormC_bound_one (ρ : SmoothCutoff) : ∃ (Crenorm : ℝ), 0 < Crenorm ∧ ∀ (lam ε : ℝ), 0 ≤ lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → |renormC2q ρ lam ε 1| ≤ ε⁻¹ ^ 2 / |Real.log ε| * (Crenorm * lam) ^ 2

The actual (3.22) estimate at q = 1, with one constant chosen before the coupling and scale. This is the completely closed base case of P-3.5a, not an output-interface theorem.