The primitive-pairing kernel and the exact Proposition 4.1 predicate

Paper: P-4.1 — Prop 4.1 statement layer — (4.2)–(4.4)

This file freezes the statement layer of Deng--Shen Proposition 4.1, equations (4.2)--(4.4). In particular:

• primitiveFullPairings n is the finite class of primitive full pairings of the paper interval [1, 2n] (represented by Fin (2 * n));
• primitiveKernel is (4.2), for arbitrary chain inputs G_j : T4 → ℝ;
• primitiveKernelInserted is the same expression with the additional factor ε² + max_{i,j} |x_i-x_j|² from (4.4);
• PrimitiveEstimateRegime, primitiveKernelMajorant, and primitiveInsertedMajorant make every constant hidden by the paper's ≲ notation explicit;
• Prop41BoundPredicate is only a Prop-valued specification. The difficult estimate is deliberately not asserted as a theorem here.

The endpoint tuple uses the already frozen assemble convention. Paper indices are shifted down by one throughout.

Primitive full pairings

def Anderson4D.primitiveFullPairings (n : ℕ) : Finset (PartialPairing (Fin (2 * n)))

Primitive full pairings of the paper interval [1, 2n].

IsFull excludes singles and IsPrimitive excludes every proper fully paired subinterval. Both conditions are needed: primitivity alone permits partial pairings.

Equations

• Anderson4D.primitiveFullPairings n = {κ : Anderson4D.PartialPairing (Fin (2 * n)) | κ.IsFull ∧ Anderson4D.IsPrimitive κ}

@[simp]

theorem Anderson4D.mem_primitiveFullPairings {n : ℕ} {κ : PartialPairing (Fin (2 * n))} : κ ∈ primitiveFullPairings n ↔ κ.IsFull ∧ IsPrimitive κ

theorem Anderson4D.primitiveFullPairings_one_card : (primitiveFullPairings 1).card = 1

At the first paper order there is exactly one full pairing. It is primitive, so the primitive sum in (4.2) has one term.

Endpoint assembly and chain edges

def Anderson4D.primitiveAssemble (n : ℕ) (hn : 1 ≤ n) (z w : T4) (v : Fin (2 * n - 2) → T4) : Fin (2 * n) → T4

Assemble x₁ = z, x₂, …, x_{2n-1}, and x_{2n} = w.

The proof hn excludes the junk arithmetic branch n = 0 and witnesses 2n = (2n-2)+2, so this is exactly the project's common assemble operation rather than a second endpoint convention.

Equations

• Anderson4D.primitiveAssemble n hn z w v j = Anderson4D.assemble z w v (Fin.cast ⋯ j)

def Anderson4D.primitiveLast (n : ℕ) (hn : 1 ≤ n) : Fin (2 * n)

The last slot x_{2n} of the primitive tuple.

Equations

• Anderson4D.primitiveLast n hn = ⟨2 * n - 1, ⋯⟩

def Anderson4D.primitiveInternalIdx (n : ℕ) (hn : 1 ≤ n) (i : Fin (2 * n - 2)) : Fin (2 * n)

The slot occupied by the internal variable with index i.

Equations

• Anderson4D.primitiveInternalIdx n hn i = Fin.cast ⋯ (Anderson4D.varIdx i)

@[simp]

theorem Anderson4D.primitiveAssemble_zero (n : ℕ) (hn : 1 ≤ n) (z w : T4) (v : Fin (2 * n - 2) → T4) : primitiveAssemble n hn z w v ⟨0, ⋯⟩ = z

@[simp]

theorem Anderson4D.primitiveAssemble_last (n : ℕ) (hn : 1 ≤ n) (z w : T4) (v : Fin (2 * n - 2) → T4) : primitiveAssemble n hn z w v (primitiveLast n hn) = w

@[simp]

theorem Anderson4D.primitiveAssemble_internal (n : ℕ) (hn : 1 ≤ n) (z w : T4) (v : Fin (2 * n - 2) → T4) (i : Fin (2 * n - 2)) : primitiveAssemble n hn z w v (primitiveInternalIdx n hn i) = v i

def Anderson4D.primitiveEdgeLeft (n : ℕ) (hn : 1 ≤ n) (j : Fin (2 * n - 1)) : Fin (2 * n)

Left endpoint of chain edge j, with paper edge indices shifted from 1..2n-1 to Fin (2n-1).

Equations

• Anderson4D.primitiveEdgeLeft n hn j = ⟨↑j, ⋯⟩

def Anderson4D.primitiveEdgeRight (n : ℕ) (hn : 1 ≤ n) (j : Fin (2 * n - 1)) : Fin (2 * n)

Right endpoint of chain edge j.

Equations

• Anderson4D.primitiveEdgeRight n hn j = ⟨↑j + 1, ⋯⟩

The two integrands in (4.2) and (4.4)

noncomputable def Anderson4D.primitiveChainProduct (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (x : Fin (2 * n) → T4) : ℝ

The chain product ∏_{j=1}^{2n-1} G_j(x_j-x_{j+1}).

Equations

• Anderson4D.primitiveChainProduct n hn G x = ∏ j : Fin (2 * n - 1), G j (x (Anderson4D.primitiveEdgeLeft n hn j) - x (Anderson4D.primitiveEdgeRight n hn j))

noncomputable def Anderson4D.primitiveCovarianceProduct (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin (2 * n))) (x : Fin (2 * n) → T4) : ℝ

The covariance product ∏_{ {i,j}∈κ } η_ε(x_i-x_j).

Every unordered pair is counted once, at its smaller endpoint.

Equations

• Anderson4D.primitiveCovarianceProduct ρ ε n κ x = ∏ i ∈ κ.pairSupport with i < κ i, ρ.etaEpsT4 ε (x i - x (κ i))

noncomputable def Anderson4D.primitiveIntegrand (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (κ : PartialPairing (Fin (2 * n))) (x : Fin (2 * n) → T4) : ℝ

The integrand of (4.2), before endpoint assembly.

Equations

• Anderson4D.primitiveIntegrand ρ ε n hn G κ x = Anderson4D.primitiveChainProduct n hn G x * Anderson4D.primitiveCovarianceProduct ρ ε n κ x

noncomputable def Anderson4D.torusTupleDiameterSq {ι : Type u_1} [Fintype ι] [Nonempty ι] (x : ι → T4) : ℝ

Squared diameter of a nonempty finite torus tuple: max_{i,j} |x_i-x_j|², with the project distance torusDistSq.

Equations

• Anderson4D.torusTupleDiameterSq x = Finset.univ.sup' ⋯ fun (i : ι) => Finset.univ.sup' ⋯ fun (j : ι) => Anderson4D.torusDistSq (x i - x j)

theorem Anderson4D.torusDistSq_sub_le_torusTupleDiameterSq {ι : Type u_1} [Fintype ι] [Nonempty ι] (x : ι → T4) (i j : ι) : torusDistSq (x i - x j) ≤ torusTupleDiameterSq x

theorem Anderson4D.torusTupleDiameterSq_nonneg {ι : Type u_1} [Fintype ι] [Nonempty ι] (x : ι → T4) : 0 ≤ torusTupleDiameterSq x

noncomputable def Anderson4D.primitiveInsertedIntegrand (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (κ : PartialPairing (Fin (2 * n))) (x : Fin (2 * n) → T4) : ℝ

The (4.4) integrand, with the paper's insertion ε² + max_{i,j}|x_i-x_j|².

Equations

• Anderson4D.primitiveInsertedIntegrand ρ ε n hn G κ x = (ε ^ 2 + Anderson4D.torusTupleDiameterSq x) * Anderson4D.primitiveIntegrand ρ ε n hn G κ x

The kernels

noncomputable def Anderson4D.primitiveKernel (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (z w : T4) : ℝ

The two-endpoint form of J_{2n,prim} in (4.2).

All 2n-2 internal variables use paperMeasure; the global coupling is λ_ε^{2n} exactly as in the paper. Bochner integrals retain mathlib's junk value off integrability; Proposition 4.1's analytic proof supplies the needed integrability.

Equations

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

noncomputable def Anderson4D.primitiveKernelInserted (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (z w : T4) : ℝ

The inserted two-endpoint kernel from (4.4).

Equations

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

noncomputable def Anderson4D.primitiveKernelDiff (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (z : T4) : ℝ

The one-variable kernel denoted J_{2n,prim}(z) in (4.3), obtained by fixing the second endpoint at the group identity.

Equations

• Anderson4D.primitiveKernelDiff ρ lam ε n hn G z = Anderson4D.primitiveKernel ρ lam ε n hn G z 0

noncomputable def Anderson4D.primitiveKernelInsertedDiff (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (z : T4) : ℝ

The one-variable inserted kernel denoted J̃_{2n,prim}(z) in (4.4).

Equations

• Anderson4D.primitiveKernelInsertedDiff ρ lam ε n hn G z = Anderson4D.primitiveKernelInserted ρ lam ε n hn G z 0

Closed structural and positivity interfaces

theorem Anderson4D.primitiveCovarianceProduct_nonneg (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin (2 * n))) (x : Fin (2 * n) → T4) : 0 ≤ primitiveCovarianceProduct ρ ε n κ x

theorem Anderson4D.primitiveChainProduct_nonneg (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)) (z : T4), 0 ≤ G j z) (x : Fin (2 * n) → T4) : 0 ≤ primitiveChainProduct n hn G x

theorem Anderson4D.primitiveIntegrand_nonneg (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)) (z : T4), 0 ≤ G j z) (κ : PartialPairing (Fin (2 * n))) (x : Fin (2 * n) → T4) : 0 ≤ primitiveIntegrand ρ ε n hn G κ x

theorem Anderson4D.primitiveInsertedIntegrand_nonneg (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)) (z : T4), 0 ≤ G j z) (κ : PartialPairing (Fin (2 * n))) (x : Fin (2 * n) → T4) : 0 ≤ primitiveInsertedIntegrand ρ ε n hn G κ x

theorem Anderson4D.primitiveKernel_nonneg (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)) (z : T4), 0 ≤ G j z) (z w : T4) : 0 ≤ primitiveKernel ρ lam ε n hn G z w

theorem Anderson4D.primitiveKernelInserted_nonneg (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)) (z : T4), 0 ≤ G j z) (z w : T4) : 0 ≤ primitiveKernelInserted ρ lam ε n hn G z w

Exact hypotheses and majorants for Proposition 4.1

def Anderson4D.IsAdmissiblePrimitiveInput (n : ℕ) (G : Fin (2 * n - 1) → T4 → ℝ) : Prop

The two hypotheses on every input G_j in Proposition 4.1: hyperoctahedral invariance and the normalized pointwise bound |G_j(z)| ≤ |z|⁻².

Equations

• Anderson4D.IsAdmissiblePrimitiveInput n G = ((∀ (j : Fin (2 * n - 1)), Anderson4D.MemEClassT4 (G j)) ∧ ∀ (j : Fin (2 * n - 1)) (z : Anderson4D.T4), |G j z| ≤ Anderson4D.invSqKer z)

noncomputable def Anderson4D.primitiveSupportIndicator (supportConstant ε : ℝ) (z : T4) : ℝ

Exact replacement for the support indicator 1_{|z| ≲ ε}.

The hidden support constant is the explicit parameter supportConstant; the squared formulation avoids a square root: torusDistSq z ≤ (supportConstant * ε)².

Equations

• Anderson4D.primitiveSupportIndicator supportConstant ε z = if Anderson4D.torusDistSq z ≤ (supportConstant * ε) ^ 2 then 1 else 0

theorem Anderson4D.primitiveSupportIndicator_nonneg (supportConstant ε : ℝ) (z : T4) : 0 ≤ primitiveSupportIndicator supportConstant ε z

@[simp]

theorem Anderson4D.primitiveSupportIndicator_eq_one {supportConstant ε : ℝ} {z : T4} (h : torusDistSq z ≤ (supportConstant * ε) ^ 2) : primitiveSupportIndicator supportConstant ε z = 1

@[simp]

theorem Anderson4D.primitiveSupportIndicator_eq_zero {supportConstant ε : ℝ} {z : T4} (h : ¬torusDistSq z ≤ (supportConstant * ε) ^ 2) : primitiveSupportIndicator supportConstant ε z = 0

def Anderson4D.PrimitiveEstimateRegime (n : ℕ) (lam ε orderConstant supportConstant C : ℝ) : Prop

The explicit parameter regime behind 1 ≤ n ≲ |log ε|.

orderConstant is the hidden constant in the order restriction and supportConstant is the (independent) hidden constant in the local indicator. The endpoint ε = 1 is retained because the requested theorem regime is 0 < ε ≤ 1; the order inequality itself makes that endpoint vacuous for n ≥ 1.

Equations

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

theorem Anderson4D.primitiveEstimateRegime_of_le_truncOrder {n : ℕ} (hn : 1 ≤ n) {lam ε supportConstant C : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hlam : 0 < lam) (hsupport : 0 < supportConstant) (hC : 0 < C) (hntrunc : n ≤ truncOrder ε) : PrimitiveEstimateRegime n lam ε 1 supportConstant C

Every order up to the paper's actual truncation A = ⌊|log ε|⌋ lies in the order-constant-one primitive regime.

This is the explicit compatibility bridge between (3.11) and Proposition 4.1; keeping it next to the regime definition prevents a smaller hidden order constant from silently breaking the final parametrix assembly.

noncomputable def Anderson4D.primitiveKernelMajorant (C lam ε supportConstant : ℝ) (n : ℕ) (z : T4) : ℝ

Exact right-hand side of (4.3): `(Cλ)^{2n}[ε⁻⁴/|log ε| · |z|⁻² 1_{|z|≤cε}

• |log ε|⁻²(|z|²+ε²)⁻³]`.

Equations

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

noncomputable def Anderson4D.primitiveInsertedMajorant (C lam ε supportConstant : ℝ) (n : ℕ) (z : T4) : ℝ

Exact right-hand side of (4.4), whose two changes from (4.3) are ε⁻⁴ → ε⁻² and decay power 3 → 2.

Equations

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

theorem Anderson4D.primitiveKernelMajorant_nonneg {C lam ε supportConstant : ℝ} {n : ℕ} {z : T4} (hC : 0 ≤ C) (hlam : 0 ≤ lam) : 0 ≤ primitiveKernelMajorant C lam ε supportConstant n z

theorem Anderson4D.primitiveInsertedMajorant_nonneg {C lam ε supportConstant : ℝ} {n : ℕ} {z : T4} (hC : 0 ≤ C) (hlam : 0 ≤ lam) : 0 ≤ primitiveInsertedMajorant C lam ε supportConstant n z

def Anderson4D.PrimitiveKernelBounds (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (supportConstant C : ℝ) : Prop

The two pointwise inequalities (4.3)--(4.4), with no hidden constants. This is a predicate, not a proved theorem.

Equations

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

def Anderson4D.Prop41BoundPredicate (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (orderConstant supportConstant C : ℝ) : Prop

Proposition 4.1 specification.

In the explicit small-scale and order regime, admissible G_j produce an E-class primitive kernel and satisfy both estimates (4.3)--(4.4). No existential constant and no ≲ notation are hidden in this predicate.

Equations

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

def Anderson4D.Proposition41 (ρ : SmoothCutoff) : Prop

Global quantifier closure of Proposition 4.1.

The three constants are chosen once, before λ, ε, the perturbative order, and the input kernels. Keeping this wrapper is essential: merely proving Prop41BoundPredicate after fixing all those parameters would allow the constants to depend on the inputs and would not formalize the paper's uniform estimate.

Equations

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