Grouped residual routing closure for R-324

This file bridges the absolutely convergent raw Fourier expansion to the paper-faithful residual-refined grouping. The raw full-pairing series is recorded first as an exact equality, without taking norms. The final consumer is indexed by refined primitive schedules, so all cancellation inside one compatible primitive fiber occurs before its routed weight is formed.

Exact raw series before regrouping

theorem Anderson4D.SmoothCutoff.summable_r324RawMomentFourierTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (α β : Z4) : Summable (ρ.r324RawMomentFourierTerm hm lam ε α β)

theorem Anderson4D.SmoothCutoff.deterministicMomentPairingSum_eq_rawMomentFourier_tsum (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (α β : Z4) : deterministicMomentPairingSum ρ lam ε m α β = ∑' (a : ℕ), ρ.r324RawMomentFourierTerm hm lam ε α β a

Exact full-pairing/Fourier reindexing. No triangle inequality is used here; the result is therefore safe to regroup by refined primitive schedule.