Documentation

Anderson4D.DetParametrix.Paper42_Moment.R324SignedFinalClosure

Final R-324 closure from the signed phase-A certificate #

The uniform and routed branches of paper (3.24) are proved by different integrations and therefore initially choose different harmless constants. This file replaces both by their maximum and enlarges the routed power base from 2 * primitiveConstant to the uniform branch's 16 * primitiveConstant. The resulting theorem consumes the two genuine upstream outputs of Steps 1--4 and concludes the literal paper bracket with one common named constant.

theorem Anderson4D.exists_deterministicMoment_paper_bound_of_refinedIntegrated_and_signedCollapse {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) :
∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4), 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → m ≤ truncOrder ε → MomentRefinedIntegratedReductionOutputAt ρ lam ε m α β primitiveConstant supportConstant → ∀ (a : ρ.SignedRoutedPrimitiveSlotCollapseData lam ε m hm primitiveConstant supportConstant), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ paperDeterministicMomentRHS outerConstant (16 * primitiveConstant) lam ε m α β

Signed constructive closure of deterministic R-324.

The first input is the integrated refined primitive collapse used by the uniform branch. The second is the signed, endpoint-case-indexed phase-A certificate used by the countable routing branch. Neither input contains a moment bound. A single outer constant, chosen before the cutoff, coupling, scale, order, and Fourier modes, controls both branches.