The full/full branch has zero nonconserved external mode

This is the frequency-conservation part of paper Section 4.2 before the Step-4 endpoint estimate. A full/full contraction has no cross-copy covariance slot. Hence every nonzero Fourier configuration forces alpha + beta = 0; at a nonzero external shift the complete refined fibre vanishes.

The configuration expansion and its conservation theorem already exist. This file only transports them through the exact full-pairing and refined finite-fibre reindexings. No estimate or triangle inequality is used.

theorem Anderson4D.SmoothCutoff.deterministicMomentContractionTerm_eq_zero_of_left_isFull (rho : SmoothCutoff) {epsilon : ℝ} (hepsilon : 0 < epsilon) (hepsilonOne : epsilon ≤ 1) {m : ℕ} (alpha beta : Z4) (e : MomentContraction m) (hexternal : alpha + beta ≠ 0) (hleft : e.fst.IsFull) : deterministicMomentContractionTerm rho epsilon m alpha beta e = 0

One full/full contraction term vanishes when the external shift is nonzero. This is the integrated Fourier-conservation statement, obtained by reusing the existing exact configuration expansion.

theorem Anderson4D.SmoothCutoff.r324RefinedPhysicalIntegral_eq_zero_of_representative_isFull (rho : SmoothCutoff) {epsilon : ℝ} (hepsilon : 0 < epsilon) (hepsilonOne : epsilon ≤ 1) {m : ℕ} (alpha beta : Z4) (p : R324RefinedScheduleIndex m) (hexternal : alpha + beta ≠ 0) (hfull : (r324RefinedScheduleRepresentative p).fst.IsFull ∧ (r324RefinedScheduleRepresentative p).snd.fst.IsFull) : r324RefinedPhysicalIntegral rho epsilon m alpha beta p = 0

A residual-refined fibre represented by two full halves vanishes at a nonzero external shift. Fullness propagates through the fibre by the already proved endpoint-signature rigidity theorem.