Paper Step 4(A): complete full/full zero-shift producer

This file is the numerical closure of the exact paper-ordered identities already proved upstream. The first incoming primitive defect pays the one ordinary-majorant endpoint loss. Every later exceptional head is absorbed by the synchronized complete budget, so no second endpoint loss is charged inside either half.

theorem Anderson4D.R324WithinHalfResidualPrefix.terminalBudgetScale_zero_eq_closedForm_of_full {rho : SmoothCutoff} {C lam eps K A : ℝ} {q : ℕ} {kappa : PartialPairing (Fin (2 * q))} {res : R324WithinHalfResidualPrefix rho lam eps kappa} (transport : res.R324WithinHalfAlternatingTransport) (terminalBudgetScale : Fin (2 * q + 1) → ℝ) (terminalReachable : R324WithinHalfBudgetScaleReachable kappa rho C lam eps K A transport.final.state terminalBudgetScale) (hkappa : kappa.IsFull) : terminalBudgetScale 0 = A ^ (2 * q + 1) * (C * lam) ^ (2 * q) * K ^ transport.final.state.processed.length

Exact terminal slot-zero ledger for a complete full-pairing half.

One complete half, with the endpoint loss paid once

theorem Anderson4D.R324WithinHalfResidualPrefix.exists_fullPairing_half_endpointZeroShift_bound (rho : SmoothCutoff) : ∃ (Cdet : ℝ), 0 < Cdet ∧ ∀ (lam eps : ℝ) (q : ℕ) (kappa : PartialPairing (Fin (2 * q))), 0 < lam → 0 < eps → eps ≤ 1 → 1 ≤ |Real.log eps| → q ≤ truncOrder eps → 1 ≤ q → kappa.IsFull → ∀ (alpha beta : Z4), alpha + beta = 0 → ‖↑(lamEps lam eps) ^ (2 * q) * ∑ tau : ReductionEndpointFiberAt kappa, deterministicFullHalfIntegral rho eps (2 * q) alpha beta ↑tau‖ ≤ paperFourthOrderModeDecay alpha * (eps⁻¹ ^ 2 * ((Cdet * lam) ^ (2 * q) / |Real.log eps|))

Paper Step 4(A), complete full-pairing half at zero conserved shift. All exact interval removals precede the norm. The displayed eps^-2 is the sole ordinary-majorant loss of this half.

Two complete halves and the actual refined physical fibre

theorem Anderson4D.exists_r324PaperFullEndpointZeroShiftWeightedMajorantBound (rho : SmoothCutoff) {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (primitiveConstant : ℝ), 0 < primitiveConstant ∧ R324PaperFullEndpointZeroShiftWeightedMajorantBound rho primitiveConstant supportConstant

Paper Step 4(A), full/full zero-shift producer. The two complete half estimates are joined by the existing exact finite-fibre product. The support-radius loss in the final inserted-majorant lower bound is absorbed once into the order-independent primitive constant.