Summation at the paper's central-frequency scale

Paper: R-324 — §4.2, Step 4 and the final summation

The central bracket produced in Step 4(B) is ⟨ε²(α+β)⟩⁻⁸. This file sums the post-collapse refined-fibre bound at exactly that scale. It deliberately does not pass through R324HdetBracketLedgerBound, whose ⟨ε(α+β)⟩⁻⁸ premise is stronger than the statement proved in the paper.

theorem Anderson4D.R324RefinedPostCollapsePaperBracketBound.refinedTermSum_le {ρ : SmoothCutoff} {K : ℝ} (h : R324RefinedPostCollapsePaperBracketBound ρ K) {ε : ℝ} (m : ℕ) (α β : Z4) (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hlog : 1 ≤ |Real.log ε|) (hm2 : 2 ≤ m) (hmtrunc : m ≤ truncOrder ε) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (hs : s ∈ momentContractionSignatures m) (r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (hr : r ∈ momentResidualChainSignaturesAt m s) : ‖momentRefinedDeterministicTermSum ρ ε m α β s r‖ ≤ ↑m ^ 8 * K ^ m * |Real.log ε| ^ (m - 1) * (r324EndpointLoss ε α β * eighthOrderFrequencyDecay (ε ^ 2 * ‖z4EuclideanFrequency (α + β)‖))

The paper-scale post-collapse estimate, expressed on the residual signature fibre used by the final finite summation.

theorem Anderson4D.r324PaperScale_pairingSum_le_of_postCollapseBracket {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (h : R324RefinedPostCollapsePaperBracketBound ρ K) (lam : ℝ) {ε : ℝ} {m : ℕ} (α β : Z4) (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hlog : 1 ≤ |Real.log ε|) (hm2 : 2 ≤ m) (hmtrunc : m ≤ truncOrder ε) : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ lamEps lam ε ^ 2 * (65536 * K) ^ m * lam ^ (2 * m - 2) * (r324EndpointLoss ε α β * eighthOrderFrequencyDecay (ε ^ 2 * ‖z4EuclideanFrequency (α + β)‖))

The paper-scale bracket sums over residual schedules and contraction signatures with the same finite counting cost as the existing final assembly. The conclusion retains ε² verbatim.