The inserted Step-1 budget for later incoming exceptional heads

After the first paired endpoint has supplied the fourth-order external decay, every later exceptional head in the literal suffix carries exactly paperSecondOrderModeDecay k * primitiveDefect k. Paper Section 4.2, Step 1 spends that multiplier on the quadratic cosine defect and therefore uses the inserted majorant (4.4), with no further eps^-2 endpoint loss.

The terminal specialization of this estimate already appears as paperDecay_mul_norm_integral_terminalPrimitiveKernelDiff_le_scaled_inserted. This file exposes precisely the same argument for an arbitrary certified literal head, so the alternating suffix can consume it one block at a time.

theorem Anderson4D.R324WithinHalfResidualPrefix.paperDecay_mul_norm_incomingExceptionalPrimitiveDefect_le_scaled_inserted {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (scale : Fin (m + 1) → ℝ) (certificate : R324WithinHalfEdgeCertificate ctx.state scale) (hε : 0 < eps) (supportConstant primitiveConstant : ℝ) (hprimitive : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (hprop : ∀ (H : Fin (2 * residualBlockOrder ctx.step.2 - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput (residualBlockOrder ctx.step.2) H → MemEClassT4 (primitiveKernelDiff rho lam eps (residualBlockOrder ctx.step.2) ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff rho lam eps (residualBlockOrder ctx.step.2) ⋯ H) ∧ PrimitiveKernelBounds rho lam eps (residualBlockOrder ctx.step.2) ⋯ H supportConstant primitiveConstant) (k : Z4) : paperSecondOrderModeDecay k * ‖incomingExceptionalPrimitiveDefect rho lam eps (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges k‖ ≤ r324WithinHalfInternalEdgeScaleProduct ctx scale * (1 / 2 * (max 1 (supportConstant ^ 2) * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam eps supportConstant (residualBlockOrder ctx.step.2) z ∂paperMeasure))

Certificate-scaled form of the paper's inserted Step-1 cosine charge at an arbitrary literal within-half head. The modulus is taken only after the primitive sum has been integrated and its sine part has vanished by MemEClassT4 symmetry.

theorem Anderson4D.R324WithinHalfResidualPrefix.norm_incomingExceptionalHeadCollapseFactor_le_scaled_inserted {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix rho lam eps pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (scale : Fin (m + 1) → ℝ) (certificate : R324WithinHalfEdgeCertificate res.state scale) (hε : 0 < eps) (supportConstant primitiveConstant : ℝ) (hprimitive : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (hprop : ∀ (H : Fin (2 * residualBlockOrder head.2 - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput (residualBlockOrder head.2) H → MemEClassT4 (primitiveKernelDiff rho lam eps (residualBlockOrder head.2) ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff rho lam eps (residualBlockOrder head.2) ⋯ H) ∧ PrimitiveKernelBounds rho lam eps (residualBlockOrder head.2) ⋯ H supportConstant primitiveConstant) (k : Z4) : ‖res.incomingExceptionalHeadCollapseFactor head tail hremaining k‖ ≤ r324WithinHalfInternalEdgeScaleProduct (res.headContext head tail hremaining) scale * (1 / 2 * (max 1 (supportConstant ^ 2) * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam eps supportConstant (residualBlockOrder head.2) z ∂paperMeasure))

The sharp later-stop estimate in the exact form used by the alternating driver multiplier.