Primitive decoder trace foundations
Abstract
Finite primitive traces retain actual readable states and acquisition boundaries.
Theorem 1.1 (Position liveness supplies every actual D cut).
Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/DecoderOperationTrace/Basic.actual_cut_exists (✓ std3). ∎
Source. Repository-derived.
Commentary.
Ready means acquire or stopped. A Cut is a finite trace over the available front(r,n), from the physical initial state with acquired zero and empty output, ending Ready at acquired n. No End event is supplied. Processing means a finite internal-only startup drain and a finite internal-only drain after every acquisition actually executed on any Record. It quantifies neither over unreachable states nor impossible acquisitions. Liveness means every position has a finite full-run witness for every Record in InD. Startup gives n=0. Deterministic path comparability and liveness beyond the current finite output force the next acquisition; its actual drain supplies the next cut. This is an explicit operational theorem. Universal correspondence to a prose machine definition, endpoint granularity require independent assessment; finite startup is derived from actual first-label competitors by processing_of_safe_live_pair.