The empty residual branch of the R-324 reduction

When both within-half contractions are full, Definition 3.1 exhausts both active carriers. Consequently the doubled residual carrier is empty, the filtered residual collapse schedule has no blocks, and its primitive-sum product is the multiplicative identity.

theorem Anderson4D.momentResidualActive_eq_empty_iff_isFull {m : ℕ} (κp κm : PartialPairing (Fin m)) : momentResidualActive κp κm = ∅ ↔ κp.IsFull ∧ κm.IsFull

The doubled residual carrier is empty exactly when both within-half pairings are full.

theorem Anderson4D.PartialPairing.IsFull.exists_fin_order_eq_two_mul {m : ℕ} {κ : PartialPairing (Fin m)} (hκ : κ.IsFull) : ∃ (q : ℕ), m = 2 * q

A full pairing of Fin m supplies the even-order witness in the exact shape used by the full/full R-324 branch.

theorem Anderson4D.nonemptyMomentResidualCollapseBlocks_eq_nil_of_isFull {m : ℕ} {κp κm : PartialPairing (Fin m)} (π : ↥κp.singles ≃ ↥κm.singles) (hp : κp.IsFull) (hm : κm.IsFull) : nonemptyMomentResidualCollapseBlocks κp κm π = []

No nonempty cross-cut collapse block survives when both within-half pairings are full.

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

The exact residual primitive-sum product is the empty product in the full/full branch.