Budget-synchronized transport stopping before an outgoing terminal

This is the retained-terminal analogue of exists_budgetSynchronizedAlternatingTransport. It follows the same literal paper schedule, alternates ordinary runs with exceptional incoming heads, and stops immediately before one prescribed last block. The exact signed endpoint-stop witness and the complete numerical budget are built together, so the multiplier bound lives on the actual stop carrier used by the outgoing Fourier identity.

structure Anderson4D.R324WithinHalfResidualPrefix.R324BudgetedEndpointStopAtTerminal {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (terminal : R322ExtractionStep m) (res : R324WithinHalfResidualPrefix rho lam eps pairing) (initialBudgetScale : Fin (m + 1) → ℝ) (mode : Z4) : Type

Exact endpoint-stop transport together with the complete budget on the same stop state.

• endpoint : R324WithinHalfEndpointStopAtTerminal terminal res
• stopBudgetScale : Fin (m + 1) → ℝ
• stopReachable : R324WithinHalfBudgetScaleReachable pairing rho C lam eps K A self.endpoint.stop.state self.stopBudgetScale
• stopCertificate : R324WithinHalfEdgeCertificate self.endpoint.stop.state self.stopBudgetScale
• multiplier_budget : ‖self.endpoint.multiplier mode‖ * initialBudgetScale 0 ≤ self.stopBudgetScale 0

theorem Anderson4D.R324WithinHalfResidualPrefix.R324BudgetedEndpointStopAtTerminal.exists_of_providers {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {mode : Z4} (heps : 0 < eps) (heps1 : 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) (headBudget : R324WithinHalfInsertedExceptionalHeadBudget rho C lam eps K pairing mode) (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) (terminal : R322ExtractionStep m) (pre : List (R322ExtractionStep m)) (hremaining : res.remaining = pre ++ [terminal]) : Nonempty (R324BudgetedEndpointStopAtTerminal terminal res budgetScale mode)

Paper-order endpoint-stop budget recursion. The named terminal itself is not consumed.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324BudgetedEndpointStopAtTerminal.completedRoute_after_outgoingTerminal {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (budgetProvider : R324WithinHalfBudgetLocalBlockProvider rho C lam eps K A pairing) (terminalData : R324ShortcutTerminalSchedule pairing) {res : R324WithinHalfResidualPrefix rho lam eps pairing} {initialBudgetScale : Fin (m + 1) → ℝ} {mode : Z4} (data : R324BudgetedEndpointStopAtTerminal terminalData.terminal res initialBudgetScale mode) (hpred : r324WithinHalfPredecessorSlot data.endpoint.stop.state terminalData.terminal ≠ 0) (cases : R324PaperHalfEndpointCases) (firstCharge : ℝ) (hfirstNonneg : 0 ≤ firstCharge) (hfirst : firstCharge ≤ initialBudgetScale 0) : have outgoing := { terminalData := terminalData, endpoint := data.endpoint }; ∃ (route : R324PaperHalfCompletedRoute pairing mode), route.cases = cases ∧ route.final = outgoing.terminalPost

Consume the retained outgoing terminal by one complete-budget update after its exact signed Fourier/primitive operation. Since the terminal predecessor is nonzero in the residual branch, slot zero is unchanged; any first-incoming charge already controlled by the stop budget therefore survives verbatim on terminalPost.