Exact factorization of the full/full R-324 contraction term

When both within-half pairings are full, their single sets are empty. Thus the cross-copy covariance product in the frozen deterministic moment integrand is the empty product. The genuine five-group physical carrier then reindexes, without changing Haar measure, as the product of the two independent flat half-carriers.

The theorem below records the resulting exact factorization at the frozen deterministicMomentContractionTerm boundary. It keeps the four endpoint characters with their original signs. Its two Integrable hypotheses are precisely the Fubini seam: they imply joint integrability of the separated product after the measure-preserving reindexing. No moment-reduction output interface and no estimate is used.

theorem Anderson4D.deterministicMomentContractionTerm_eq_fullHalfIntegral_mul (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hp : κp.IsFull) (hm : κm.IsFull) (hleft : MeasureTheory.Integrable (fun (p : T4 × T4 × (Fin m → T4)) => charT4 α p.1 * charT4 β p.2.1 * ↑(detIntegrand ρ ε m κp (assemble p.1 p.2.1 p.2.2))) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure)))) (hright : MeasureTheory.Integrable (fun (p : T4 × T4 × (Fin m → T4)) => charT4 (-α) p.1 * charT4 (-β) p.2.1 * ↑(detIntegrand ρ ε m κm (assemble p.1 p.2.1 p.2.2))) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure)))) : deterministicMomentContractionTerm ρ ε m α β ⟨κp, ⟨κm, π⟩⟩ = (∫ (p : T4 × T4 × (Fin m → T4)), charT4 α p.1 * charT4 β p.2.1 * ↑(detIntegrand ρ ε m κp (assemble p.1 p.2.1 p.2.2)) ∂paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure))) * ∫ (p : T4 × T4 × (Fin m → T4)), charT4 (-α) p.1 * charT4 (-β) p.2.1 * ↑(detIntegrand ρ ε m κm (assemble p.1 p.2.1 p.2.2)) ∂paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure))

A full/full frozen contraction is exactly the product of its two independent half-integrals. The left endpoints retain modes α, β, while the right endpoints retain the conjugate modes -α, -β.