Complete-budget control of the incoming alternating suffix

Paper Section 4.2 removes every ordinary interval before taking a norm. A slot-zero-fed head is then Fourier-collapsed and the literal suffix resumes. The analytic driver already implements that alternation. This file runs its numerical complete budget along the same literal heads.

The useful invariant is deliberately small: the norm of the accumulated exceptional multiplier, times the current slot-zero budget, is bounded by the terminal slot-zero budget. At an ordinary run slot zero is untouched; at an exceptional head the inserted cosine estimate is exactly one complete budget update after enlarging the universal one-block constant once. Thus no exceptional suffix block pays a second eps^-2 endpoint loss.

Enlarging the one-block constant

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfLocalBlockProvider.mono_K {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {K' : ℝ} (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hKK' : K ≤ K') (provider : R324WithinHalfLocalBlockProvider rho C lam eps K pairing) : R324WithinHalfLocalBlockProvider rho C lam eps K' pairing

A local analytic block provider remains valid after enlarging its nonnegative universal one-block constant.

The sharp exceptional-head input

def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfInsertedExceptionalHeadBudget (rho : SmoothCutoff) (C lam eps K : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) (k : Z4) : Prop

Every exceptional head spends its inserted-cosine charge inside the same complete-budget update used for an ordinary head.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.R324WithinHalfResidualPrefix.r324WithinHalfInsertedExceptionalHeadBudget_of_prop41 {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (hε : 0 < eps) (supportConstant primitiveConstant : ℝ) (hprimitive : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (hprop : ∀ (res : R324WithinHalfResidualPrefix rho lam eps pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (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) (hcharge : ∀ (n : ℕ), 1 ≤ n → 1 / 2 * (max 1 (supportConstant ^ 2) * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam eps supportConstant n z ∂paperMeasure) ≤ (C * lam) ^ (2 * n) * K) (k : Z4) : R324WithinHalfInsertedExceptionalHeadBudget rho C lam eps K pairing k

Proposition 4.1's inserted estimate supplies the exceptional-head budget once its scalar inserted integral is covered by K.

Slot-zero budget along an ordinary trace

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.exists_terminalBudget_zero_eq {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (budgetProvider : R324WithinHalfBudgetLocalBlockProvider rho C lam eps K A pairing) {res : R324WithinHalfResidualPrefix rho lam eps pairing} {analyticScale budgetScale : Fin (m + 1) → ℝ} (trace : res.R324WithinHalfCertifiedAnalyticTrace analyticScale) (hordinary : trace.OrdinaryAlong) (budgetReachable : R324WithinHalfBudgetScaleReachable pairing rho C lam eps K A res.state budgetScale) (budgetCertificate : R324WithinHalfEdgeCertificate res.state budgetScale) : ∃ (terminalBudgetScale : Fin (m + 1) → ℝ), R324WithinHalfBudgetScaleReachable pairing rho C lam eps K A trace.terminalPrefix.state terminalBudgetScale ∧ R324WithinHalfEdgeCertificate trace.terminalPrefix.state terminalBudgetScale ∧ terminalBudgetScale 0 = budgetScale 0

A complete budget run along an all-ordinary analytic trace leaves slot zero unchanged. No comparison of analytic and budget scales is needed in this base case; they merely traverse the same literal residual states.

Budget-synchronized alternating transport

theorem Anderson4D.R324WithinHalfResidualPrefix.exists_budgetSynchronizedAlternatingTransport {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (hε : 0 < eps) (hε1 : eps ≤ 1) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hK : 0 ≤ K) (hA : 1 ≤ A) (analyticProvider : R324WithinHalfLocalBlockProvider rho C lam eps K pairing) (budgetProvider : R324WithinHalfBudgetLocalBlockProvider rho C lam eps K A pairing) (res : R324WithinHalfResidualPrefix rho lam eps pairing) (analyticScale budgetScale : Fin (m + 1) → ℝ) (analyticCertificate : R324WithinHalfEdgeCertificate res.state analyticScale) (budgetReachable : R324WithinHalfBudgetScaleReachable pairing rho C lam eps K A res.state budgetScale) (budgetCertificate : R324WithinHalfEdgeCertificate res.state budgetScale) (hscale : ∀ (edge : Fin (m + 1)), analyticScale edge ≤ budgetScale edge) (k : Z4) (headBudget : R324WithinHalfInsertedExceptionalHeadBudget rho C lam eps K pairing k) : ∃ (transport : res.R324WithinHalfAlternatingTransport) (terminalBudgetScale : Fin (m + 1) → ℝ), R324WithinHalfBudgetScaleReachable pairing rho C lam eps K A transport.final.state terminalBudgetScale ∧ R324WithinHalfEdgeCertificate transport.final.state terminalBudgetScale ∧ ‖transport.multiplier k‖ * budgetScale 0 ≤ terminalBudgetScale 0

Paper-order alternating budget. There is an exact alternating transport whose exceptional multiplier is paid by the complete numerical budget on the same literal schedule. The invariant is the telescoping slot-zero inequality

norm multiplier * currentBudget(0) <= terminalBudget(0).

Ordinary runs do not touch slot zero. At a retained exceptional head the predecessor is slot zero, and the head budget is dominated by the complete update because the untouched outgoing scale is A >= 1.

Starting the alternating suffix at the paper's first incoming head

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.R324IncomingExceptionalBudgetedStopTraceAssembly.exists_budgetSynchronizedAlternatingTransport_afterHead {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (pack : R324IncomingExceptionalBudgetedStopTraceAssembly pairing) (hε : 0 < eps) (hε1 : eps ≤ 1) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hK : 0 ≤ K) (hA : 1 ≤ A) (analyticProvider : R324WithinHalfLocalBlockProvider rho C lam eps K pairing) (budgetProvider : R324WithinHalfBudgetLocalBlockProvider rho C lam eps K A pairing) (k : Z4) (headBudget : R324WithinHalfInsertedExceptionalHeadBudget rho C lam eps K pairing k) : ∃ (transport : (pack.data.trace.stopPrefix.afterHead pack.data.terminal pack.data.suffix ⋯).R324WithinHalfAlternatingTransport) (terminalBudgetScale : Fin (m + 1) → ℝ), R324WithinHalfBudgetScaleReachable pairing rho C lam eps K A transport.final.state terminalBudgetScale ∧ R324WithinHalfEdgeCertificate transport.final.state terminalBudgetScale ∧ ‖transport.multiplier k‖ * pack.afterHeadBudgetScale 0 ≤ terminalBudgetScale 0

Consumer form for the canonical incoming stop. After the first ordinary primitive defect has been exposed, the remaining literal suffix is transported with the same complete budget. This theorem introduces no new estimate; it only connects the stopped package to the alternating theorem above.