The first primitive-pairing order

Paper §5 begins the proof of Proposition 4.1 by separating n = 1. At that order there are no internal variables and exactly one primitive full pairing. This file proves the resulting closed formulas for both the ordinary and diameter-inserted kernels. Thus the base case is reduced honestly to the cutoff covariance bounds, with no lattice-tree machinery.

def Anderson4D.pairingFinTwo : PartialPairing (Fin 2)

The unique full pairing of two indices.

Equations

• Anderson4D.pairingFinTwo = { toFun := Fin.rev, involutive := Anderson4D.pairingFinTwo._proof_1 }

theorem Anderson4D.primitiveFullPairings_one_eq : primitiveFullPairings 1 = {pairingFinTwo}

@[simp]

theorem Anderson4D.pairingFinTwo_zero : pairingFinTwo 0 = 1

@[simp]

theorem Anderson4D.pairingFinTwo_one : pairingFinTwo 1 = 0

theorem Anderson4D.pairingFinTwo_lowerSupport : {i ∈ pairingFinTwo.pairSupport | i < pairingFinTwo i} = {0}

theorem Anderson4D.primitiveKernel_one (ρ : SmoothCutoff) (lam ε : ℝ) (G : Fin 1 → T4 → ℝ) (z w : T4) : primitiveKernel ρ lam ε 1 ⋯ G z w = lamEps lam ε ^ 2 * (G 0 (z - w) * ρ.etaEpsT4 ε (z - w))

Closed n = 1 formula quoted at the start of paper §5.

theorem Anderson4D.primitiveKernelInserted_one (ρ : SmoothCutoff) (lam ε : ℝ) (G : Fin 1 → T4 → ℝ) (z w : T4) : primitiveKernelInserted ρ lam ε 1 ⋯ G z w = lamEps lam ε ^ 2 * ((ε ^ 2 + torusDistSq (z - w)) * (G 0 (z - w) * ρ.etaEpsT4 ε (z - w)))

Closed n = 1 formula with the (4.4) diameter insertion.