Dependency-closed pairing collapse for Proposition 3.4

This file connects the three head cases to the current random-parametrix and Wick APIs. It contains the finite reindexing and creation--contraction identities which require no analytic interchange of integrals. The remaining step in the full kernel identity (3.16) is an analytic identification of each case-(3) integral with detJ times the external randRI.

def Anderson4D.PartialPairing.caseThreeQ {m : ℕ} (κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix }) : ℕ

The minimal prefix order of a case-(3) pairing.

Equations

• Anderson4D.PartialPairing.caseThreeQ κ = (↑κ).firstFullyPairedHeadQ ⋯

theorem Anderson4D.PartialPairing.caseThreeQ_spec {m : ℕ} (κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix }) : (↑κ).IsFullyPairedHeadPrefix (caseThreeQ κ)

theorem Anderson4D.PartialPairing.caseThreeQ_mem_range {m : ℕ} (κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix }) : caseThreeQ κ ∈ Finset.Icc 1 ((m + 1) / 2)

theorem Anderson4D.PartialPairing.sum_caseThree_by_q {m : ℕ} {R : Type u_1} [AddCommMonoid R] (f : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix } → R) : ∑ κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix }, f κ = ∑ q ∈ Finset.Icc 1 ((m + 1) / 2), ∑ κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix } with caseThreeQ κ = q, f κ

Regroup the case-(3) contribution by the uniquely determined minimal prefix length 2q.

theorem Anderson4D.PartialPairing.sum_headCases_collapse {m : ℕ} {R : Type u_1} [AddCommMonoid R] (f : PartialPairing (Fin (m + 1)) → R) (fSingle : { κ : PartialPairing (Fin (m + 1)) // κ.HeadIsSingle } → R) (fRegular : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedNoPrefix } → R) (fCounter : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix } → R) (hSingle : ∀ (κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadIsSingle }), f ↑κ = fSingle κ) (hRegular : ∀ (κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedNoPrefix }), f ↑κ = fRegular κ) (hCounter : ∀ (κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix }), f ↑κ = fCounter κ) : ∑ κ : PartialPairing (Fin (m + 1)), f κ = ∑ κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadIsSingle }, fSingle κ + ∑ κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedNoPrefix }, fRegular κ + ∑ κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix }, fCounter κ

A generic collapse theorem: once the contribution is identified on each of the three disjoint classes, the full pairing sum is their sum.

The minimal prefix is a non-split full pairing

def Anderson4D.PartialPairing.HeadPrefixDecomposition.collapsePrefixOrderIso {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (d : κ.HeadPrefixDecomposition) : Fin (2 * d.q) ≃o ↥(headEvenPrefix m d.q)

The concrete cast-based order isomorphism from Fin (2q) to the ambient first 2q positions. Unlike an abstract sorted enumeration, this has definitionally transparent index values.

Equations

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

def Anderson4D.PartialPairing.HeadPrefixDecomposition.collapsePrefixPairing {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (d : κ.HeadPrefixDecomposition) : PartialPairing (Fin (2 * d.q))

The first block σ₁, using the transparent cast reindexing.

Equations

• d.collapsePrefixPairing = (Anderson4D.PartialPairing.congr d.collapsePrefixOrderIso.symm.toEquiv) (κ.restrictTo ⋯)

theorem Anderson4D.PartialPairing.HeadPrefixDecomposition.collapsePrefixPairing_isFull {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (d : κ.HeadPrefixDecomposition) : d.collapsePrefixPairing.IsFull

@[simp]

theorem Anderson4D.PartialPairing.HeadPrefixDecomposition.collapsePrefixPairing_apply_val {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (d : κ.HeadPrefixDecomposition) (i : Fin (2 * d.q)) : ↑(d.collapsePrefixPairing i) = ↑(κ (Fin.castLE ⋯ i))

theorem Anderson4D.PartialPairing.HeadPrefixDecomposition.ambientFullyPaired_of_collapsePrefix {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (d : κ.HeadPrefixDecomposition) {r : ℕ} (hr : 2 * r ≤ 2 * d.q) (h : IsFullyPairedOn d.collapsePrefixPairing {i : Fin (2 * d.q) | ↑i < 2 * r}) : IsFullyPairedOn κ (headEvenPrefix m r)

A fully paired prefix of the collapsed first block pulls back to the same zero-based prefix of the ambient pairing.

theorem Anderson4D.PartialPairing.HeadPrefixDecomposition.collapsePrefixPairing_isNonSplit {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (d : κ.HeadPrefixDecomposition) : IsNonSplit d.collapsePrefixPairing

Minimality of the first fully paired head prefix says exactly that its restriction belongs to the paper's non-concatenation class. This is the combinatorial bridge from case (3) of Proposition 3.4 to the indexing set in renormC2q.

def Anderson4D.PartialPairing.caseThreeDecomposition {m : ℕ} (κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix }) : (↑κ).HeadPrefixDecomposition

The canonical minimal-prefix decomposition attached to a case-(3) pairing.

Equations

• Anderson4D.PartialPairing.caseThreeDecomposition κ = (↑κ).headPrefixDecomposition ⋯

@[simp]

theorem Anderson4D.PartialPairing.caseThreeDecomposition_q {m : ℕ} (κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix }) : (caseThreeDecomposition κ).q = caseThreeQ κ

theorem Anderson4D.PartialPairing.caseThree_prefix_isNonSplit {m : ℕ} (κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix }) : IsNonSplit (caseThreeDecomposition κ).collapsePrefixPairing

In canonical case-(3) data, the internal pairing σ₁ is an admissible summand of renormC2q.

theorem Anderson4D.PartialPairing.caseThree_prefix_mem_nonSplit_filter {m : ℕ} (κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix }) : (caseThreeDecomposition κ).collapsePrefixPairing ∈ Finset.filter IsNonSplit Finset.univ

Wick creation--contraction at the head

theorem Anderson4D.xi_mul_wickAt_eq_create_add_contract (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) (z : T4) (ω : M.Ω) : M.xiEps ρ ε ω z * wickAt M ρ ε κ xt ω = wickPolynomial (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) (fun (x : T4) (ω' : M.Ω) => M.xiEps ρ ε ω' x) (z :: wickAtSingleLabels κ xt) ω + ∑ j : Fin (wickAtSingleLabels κ xt).length, ρ.etaEpsT4 ε (z - (wickAtSingleLabels κ xt).get j) * wickPolynomial (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) (fun (x : T4) (ω' : M.Ω) => M.xiEps ρ ε ω' x) ((wickAtSingleLabels κ xt).eraseIdx ↑j) ω

The exact Wick-theorem step used before the three pairing cases in the proof of (3.16), specialized to the mollified field and its covariance. No symmetry or probabilistic hypothesis is needed.

Parametrix finite-sum collapse

theorem Anderson4D.parametrixP_succ_eq_headCases (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (x y : T4) (ω : M.Ω) : parametrixP M ρ lam ε (m + 1) x y ω = ∑ κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadIsSingle }, randRI M ρ lam ε (m + 1) (↑κ) x y ω + ∑ κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedNoPrefix }, randRI M ρ lam ε (m + 1) (↑κ) x y ω + ∑ κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix }, randRI M ρ lam ε (m + 1) (↑κ) x y ω

P_{m+1} split into exactly the three classes in paper Prop. 3.4.

theorem Anderson4D.parametrixP_succ_eq_headCases_by_q (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (x y : T4) (ω : M.Ω) : parametrixP M ρ lam ε (m + 1) x y ω = ∑ κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadIsSingle }, randRI M ρ lam ε (m + 1) (↑κ) x y ω + ∑ κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedNoPrefix }, randRI M ρ lam ε (m + 1) (↑κ) x y ω + ∑ q ∈ Finset.Icc 1 ((m + 1) / 2), ∑ κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix } with PartialPairing.caseThreeQ κ = q, randRI M ρ lam ε (m + 1) (↑κ) x y ω

The same split with case (3) already regrouped by its unique q. This is the finite-sum shape of the counterterm sum in (3.16).