Bridge from wickAt to recursive Wick polynomials

The random parametrix layer defines its Wick factor directly as a sum over partial pairings of the outer pairing's single indices. This file identifies that formula with explicitPartialPairingWick and hence with wickPolynomial.

theorem Anderson4D.PartialPairing.card_representatives_eq_card_pairs {α : Type u_1} [Fintype α] [LinearOrder α] (κ : PartialPairing α) : κ.representatives.card = κ.pairs.card

In a finite linear order, the smaller endpoints of the nontrivial two-cycles are in bijection with the unordered pairs.

theorem Anderson4D.PartialPairing.prod_neg_eq_neg_one_pow_pairs_mul {α : Type u_1} [Fintype α] [LinearOrder α] (κ : PartialPairing α) (c : α → ℝ) : ∏ i ∈ κ.representatives, -c i = (-1) ^ κ.pairs.card * ∏ i ∈ κ.representatives, c i

Pulling one minus sign out of every representative covariance produces the sign convention used by wickAt.

def Anderson4D.wickAtSingleLabels {m : ℕ} (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) : List T4

The single indices of κ, evaluated in increasing order at the corresponding internal positions of xt.

Equations

• Anderson4D.wickAtSingleLabels κ xt = List.ofFn fun (j : Fin κ.singles.card) => xt (Anderson4D.varIdx ((κ.singles.orderEmbOfFin ⋯) j))

theorem Anderson4D.explicitPartialPairingWick_finsetSubtype_eq_list {α : Type u_1} {ι : Type u_2} {Ω : Type u_3} [LinearOrder α] (s : Finset α) (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (v : ↥s → ι) (ω : Ω) : explicitPartialPairingWick C X v ω = explicitPartialPairingWickList C X (List.ofFn fun (j : Fin s.card) => v ((s.orderIsoOfFin ⋯) j)) ω

A generic ordered-finset bridge from a partial-pairing sum on the subtype carrier to the list-indexed explicit Wick expansion.

theorem Anderson4D.wickAt_summand_eq_partialPairingWickWeight (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) (ω : M.Ω) (κ' : PartialPairing ↥κ.singles) : ((-1) ^ κ'.pairs.card * ∏ i ∈ κ'.pairSupport with i < κ' i, ρ.etaEpsT4 ε (xt (varIdx ↑i) - xt (varIdx ↑(κ' i)))) * ∏ i ∈ κ'.singles, M.xiEps ρ ε ω (xt (varIdx ↑i)) = partialPairingWickWeight (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) (fun (x : T4) (ω' : M.Ω) => M.xiEps ρ ε ω' x) (fun (i : ↥κ.singles) => xt (varIdx ↑i)) κ' ω

The summand in wickAt is precisely the standard explicit Wick weight: its external sign is the product of the minus signs on representative covariances.

theorem Anderson4D.wickAt_eq_explicitPartialPairingWick (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) (ω : M.Ω) : wickAt M ρ ε κ xt ω = explicitPartialPairingWick (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) (fun (x : T4) (ω' : M.Ω) => M.xiEps ρ ε ω' x) (fun (i : ↥κ.singles) => xt (varIdx ↑i)) ω

wickAt is the explicit partial-pairing Wick expansion on the ordered subtype of the original pairing's single indices.

theorem Anderson4D.wickAt_eq_wickPolynomial (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) (ω : M.Ω) : wickAt M ρ ε κ xt ω = wickPolynomial (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) (fun (x : T4) (ω' : M.Ω) => M.xiEps ρ ε ω' x) (wickAtSingleLabels κ xt) ω

P-3.4 Wick bridge. The explicit sub-pairing formula used by Parametrix.Random.wickAt is exactly the recursive Wick polynomial of the noise values at the original pairing's single indices, enumerated in their ambient order.

theorem Anderson4D.wickAt_eq_chaosProjProduct (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) (ω : M.Ω) : wickAt M ρ ε κ xt ω = chaosProjProduct κ.singles.card (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) (fun (x : T4) (ω' : M.Ω) => M.xiEps ρ ε ω' x) (wickAtSingleLabels κ xt) ω

The random factor used in randRI is literally the degree |singles κ| finite-product chaos projection. Together with GaussianPolynomialLaw.integral_chaosProjProduct_mul_eq_zero_of_ne, this closes the minimal Projₖ API required by (2.4) and (3.2).