The Steps 2--3 dichotomy: cross covariances, or none at all

Paper: R-324 — §4.2 Steps 2–3 — the cross-covariance dichotomy

The proved two-half physical collapse (twoHalf_lamEps_pow_integral_eq_initialNested) is stated at a selected residual cross-covariance slot

`R324ResidualCovarianceSlot κp = ↥κp.singles`,

so it cannot be instantiated when the left half's pairing is full. That is not a gap: a full left half means the contraction has no cross-copy covariances at all, the two halves of (4.18) are independent, and the proved deterministicMomentContractionTerm_eq_fullHalfIntegral_mul factors the term outright.

This module records the dichotomy and its two elementary supports: the two halves have equally many singles (they are matched by π), and on a full half the cross-covariance product is the empty product.

theorem Anderson4D.r324_singles_card_eq {m : ℕ} {κp κm : PartialPairing (Fin m)} (π : ↥κp.singles ≃ ↥κm.singles) : κp.singles.card = κm.singles.card

The two halves of a contraction entity have equally many singles: π matches them.

theorem Anderson4D.r324_isFull_left_iff_right {m : ℕ} {κp κm : PartialPairing (Fin m)} (π : ↥κp.singles ≃ ↥κm.singles) : κp.IsFull ↔ κm.IsFull

One half of a contraction entity is full exactly when the other is.

theorem Anderson4D.momentCrossCovarianceProduct_eq_one_of_isFull (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} {κp κm : PartialPairing (Fin m)} (π : ↥κp.singles ≃ ↥κm.singles) (hp : κp.IsFull) (v : Fin (2 * m) → T4) : momentCrossCovarianceProduct ρ ε m κp κm π v = 1

On a full half the cross-copy covariance product is the empty product.

theorem Anderson4D.r324SinglesDichotomy {m : ℕ} {κp κm : PartialPairing (Fin m)} (π : ↥κp.singles ≃ ↥κm.singles) : κp.IsFull ∧ κm.IsFull ∨ Nonempty (R324ResidualCovarianceSlot κp)

The Steps 2--3 dichotomy.

At any contraction entity (κp, κm, π) either both halves are fully paired — so there are no cross-copy covariances and the two halves of (4.18) are independent — or the left half has a single, which is exactly the residual covariance slot the two-half nested bridge consumes. The disjunction is exhaustive, so Steps 2--3 may branch on it.

theorem Anderson4D.r324SinglesDichotomy_entity {m : ℕ} (e : MomentContraction m) : e.fst.IsFull ∧ e.snd.fst.IsFull ∨ Nonempty (R324ResidualCovarianceSlot e.fst)

Entity-indexed form of the dichotomy.