Final deterministic closure for R-324

This module combines the two paper-faithful outputs of Section 4.2:

• the integrated residual-refined primitive-collapse output from Steps 1--3;
• the countable central-frequency routing output from Step 4.

In particular, the uniform branch is derived from the integrated scalar majorant. The stronger pointwise-density interface MomentUniformReductionOutputAt is not used.

Uniform branch from the integrated refined collapse

theorem Anderson4D.exists_deterministicMoment_uniform_bound_of_refinedIntegratedReduction {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4), 0 ≤ lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 1 ≤ m → MomentRefinedIntegratedReductionOutputAt ρ lam ε m α β primitiveConstant supportConstant → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ lamEps lam ε ^ 2 * outerConstant * (16 * primitiveConstant * lam) ^ (2 * m - 2)

The integrated residual-refined collapse implies the uniform branch of paper (3.24). Both finite schedule counts have already been absorbed by C ↦ 16 C in deterministicMomentPairingSum_le_integral_insertedMajorant_of_refined. The radial constants are selected before any cutoff, scale, order, or Fourier mode.

Exact paper-bracket closure

theorem Anderson4D.exists_deterministicMoment_paper_bound_of_refinedIntegrated_and_countable {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4), 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → 1 ≤ m → MomentRefinedIntegratedReductionOutputAt ρ lam ε m α β primitiveConstant supportConstant → CountableCentralRoutedMomentReductionOutput ρ lam ε m α β (lamEps lam ε ^ 2 * outerConstant * (16 * primitiveConstant * lam) ^ (2 * m - 2) * r324EndpointLoss ε α β) → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ paperDeterministicMomentRHS outerConstant (16 * primitiveConstant) lam ε m α β

Countable-series closure of deterministic R-324.

The first input is the integrated residual-refined collapse. The second input is the countable central-frequency decomposition with its aggregate endpoint budget. Together they give the exact paper bracket min (1, ⟨α⟩⁻⁴ ⟨β⟩⁻⁴ ⟨ε²(α+β)⟩⁻⁸), with the coupling and order dependence λ_ε² C ((16 C₀) λ)^(2m-2).