Cross contractions for wickAt

This file transports the generic list-indexed Wick orthogonality output to the paper's sum over bijections between the single sets of two partial pairings.

theorem Anderson4D.crossWickList_wickAtSingleLabels_eq_crossSingles {m : ℕ} (κp κm : PartialPairing (Fin m)) (xtp xtm : Fin (m + 2) → T4) (C : T4 → T4 → ℝ) : crossWickList C (wickAtSingleLabels κp xtp) (wickAtSingleLabels κm xtm) = crossSinglesEquivCovarianceSum κp κm fun (i : ↥κp.singles) (j : ↥κm.singles) => C (xtp (varIdx ↑i)) (xtm (varIdx ↑j))

The cross-contraction list sum for two wickAt label lists is exactly the finite sum over bijections between the two single-index subtypes.