Complete budget at the paper's incoming exceptional stop #

The analytic stop trace and the complete numerical budget follow the same literal prefix of the Section 4.2 schedule. This file synchronizes those two already-established recursions. It introduces no estimate: the budget provider is simply called at each head genuinely consumed by the stop trace, and the resulting reachability witness and edge certificate are retained at the exact analytic stopping state.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.exists_budgetScale_at_stop {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {suffix : List (R322ExtractionStep m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} {analyticScale budgetScale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeStepTrace terminal suffix res analyticScale) (provider : R324WithinHalfBudgetLocalBlockProvider rho C lam eps K A pairing) (reachable : R324WithinHalfBudgetScaleReachable pairing rho C lam eps K A res.state budgetScale) (certificate : R324WithinHalfEdgeCertificate res.state budgetScale) :

∃ (stopBudgetScale : Fin (m + 1) → ℝ), R324WithinHalfBudgetScaleReachable pairing rho C lam eps K A trace.stopPrefix.state stopBudgetScale ∧ R324WithinHalfEdgeCertificate trace.stopPrefix.state stopBudgetScale

Run the complete-budget provider along exactly the heads already certified by an analytic stop-before-step trace. In particular, neither the retained terminal nor any part of its suffix is consumed.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.exists_completeBudget_at_stop {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly pairing initialScale) (provider : R324WithinHalfBudgetLocalBlockProvider rho C lam eps K A pairing) (initialCertificate : R324WithinHalfEdgeCertificate (r324InitialWithinHalfEdgeState m) fun (x : Fin (m + 1)) => A) :

∃ (stopBudgetScale : Fin (m + 1) → ℝ), R324WithinHalfBudgetScaleReachable pairing rho C lam eps K A data.trace.stopPrefix.state stopBudgetScale ∧ R324WithinHalfEdgeCertificate data.trace.stopPrefix.state stopBudgetScale

Consumer form at the incoming exceptional package selected by the paper: start from the uniform all-Green budget and synchronize it with the already-built analytic prefix.

A synchronized, pointwise-dominating stop package #

The light stop trace type intentionally permits an arbitrary certified nextScale; consequently a pointwise comparison with the canonical complete budget cannot be recovered from an already packaged trace. The endpoint argument needs that comparison, so the following package builds the analytic and complete-budget prefixes synchronously from the same literal pre list. This is the stopped-prefix analogue of R324CompatibleAnalyticBudgetTrace.exists_of_providers.

source

structure Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.R324IncomingExceptionalBudgetedStopTraceAssembly {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} (pairing : PartialPairing (Fin m)) :

Type

An incoming exceptional stop together with the canonical complete budget on the same physical residual state.

data : R324IncomingExceptionalStopTraceAssembly pairing fun (x : Fin (m + 1)) => A
stopBudgetScale : Fin (m + 1) → ℝ
budgetReachable : R324WithinHalfBudgetScaleReachable pairing rho C lam eps K A self.data.trace.stopPrefix.state self.stopBudgetScale
budgetCertificate : R324WithinHalfEdgeCertificate self.data.trace.stopPrefix.state self.stopBudgetScale
stopScale_le (edge : Fin (m + 1)) : self.data.stopScale edge ≤ self.stopBudgetScale edge
stopBudget_zero_eq_base : self.stopBudgetScale 0 = A

Instances For

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.R324IncomingExceptionalBudgetedStopTraceAssembly.analyticUpdate_mono {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix rho lam eps pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (small large : Fin (m + 1) → ℝ) (hsmall : R324WithinHalfEdgeCertificate res.state small) (hlarge : R324WithinHalfEdgeCertificate res.state large) (hle : ∀ (edge : Fin (m + 1)), small edge ≤ large edge) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hK : 0 ≤ K) (edge : Fin (m + 1)) :

r324WithinHalfUpdatedEdgeScale (res.headContext head tail hremaining) small C lam K edge ≤ r324WithinHalfUpdatedEdgeScale (res.headContext head tail hremaining) large C lam K edge

Monotonicity of the signed analytic scale update.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.R324IncomingExceptionalBudgetedStopTraceAssembly.analyticUpdate_le_budgetUpdate {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix rho lam eps pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (analyticScale budgetScale : Fin (m + 1) → ℝ) (analyticCertificate : R324WithinHalfEdgeCertificate res.state analyticScale) (budgetCertificate : R324WithinHalfEdgeCertificate res.state budgetScale) (budgetReachable : R324WithinHalfBudgetScaleReachable pairing rho C lam eps K A res.state budgetScale) (hle : ∀ (edge : Fin (m + 1)), analyticScale edge ≤ budgetScale edge) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hK : 0 ≤ K) (hA : 1 ≤ A) (edge : Fin (m + 1)) :

r324WithinHalfUpdatedEdgeScale (res.headContext head tail hremaining) analyticScale C lam K edge ≤ res.budgetUpdatedEdgeScale head tail hremaining budgetScale C lam K edge

One complete-budget update dominates the simultaneous signed update. The only extra factor is the untouched outgoing Green scale, exactly A.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.R324IncomingExceptionalBudgetedStopTraceAssembly.exists_pairedStopBefore {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hK : 0 ≤ K) (hA : 1 ≤ A) (hε : 0 < eps) (hε1 : eps ≤ 1) (analyticProvider : R324WithinHalfLocalBlockProvider rho C lam eps K pairing) (budgetProvider : R324WithinHalfBudgetLocalBlockProvider rho C lam eps K A pairing) (terminal : R322ExtractionStep m) (suffix pre : List (R322ExtractionStep m)) (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) (hle : ∀ (edge : Fin (m + 1)), analyticScale edge ≤ budgetScale edge) (hremaining : res.remaining = pre ++ terminal :: suffix) :

∃ (trace : R324WithinHalfStopBeforeStepTrace terminal suffix res analyticScale) (stopBudgetScale : Fin (m + 1) → ℝ), R324WithinHalfBudgetScaleReachable pairing rho C lam eps K A trace.stopPrefix.state stopBudgetScale ∧ R324WithinHalfEdgeCertificate trace.stopPrefix.state stopBudgetScale ∧ (∀ (edge : Fin (m + 1)), trace.stopScale edge ≤ stopBudgetScale edge) ∧ (trace.OrdinaryAlong → stopBudgetScale 0 = budgetScale 0)

Build both stopped prefixes along one literal proper-prefix list.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.R324IncomingExceptionalBudgetedStopTraceAssembly.R324WithinHalfStopBeforeStepTrace.ordinaryAlong_of_terminal_left_eq_zero {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {suffix : List (R322ExtractionStep m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} {scale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeStepTrace terminal suffix res scale) (hleft : ↑terminal.1.1 = 0) :

trace.OrdinaryAlong ∧ terminal.1.1 ∈ res.state.active

A stop before a retained block whose left endpoint is vertex zero is ordinary along every genuinely consumed head. The retained zero vertex is still active after the whole prefix; hence it was active before each earlier head, while disjointness from that head forces the head to start strictly to its right. Its internal edge slot is therefore a nonzero predecessor candidate.

source