finitePrefix
plain-language theorem explainer
Finite prefixes cut the first n distinction acts out of a completed (infinite) ledger and package them as an ordinary finite trace. Trace-closure and canonical-ledger arguments cite this cut whenever they need a length-n approximation. The definition is plain recursion on length: empty at zero, one extension by the n-th act at each successor.
Claim. Given a completed trace $S$ (an infinite sequence of distinction acts $S(k)$ for $k\in\mathbb{N}$) and $n\in\mathbb{N}$, the finite prefix of length $n$ is the finite trace built by starting from the empty trace and successively adjoining $S(0),\ldots,S(n-1)$.
background
In the Primitive Recognition Calculus, a finite trace is the inductive type with constructors empty and extend-by-one-distinction-act (K2.4). A completed trace is the closure object: an infinite ledger actAt : Nat → DistinctionAct (K4.13/R9), not a finite δ-only trace.
The TraceClosure module studies how infinite ledgers relate to their finite approximations. Finite prefixes are the bridge: every completed ledger projects to a coherent family of finite traces of every length.
Upstream, Trace supplies the inductive carrier; CompletedTrace supplies the infinite act sequence. Successor on Nat indexes successive extensions.
proof idea
Definitional recursion on the length argument, not a tactic proof. At zero the prefix is the empty trace. At successor n the prefix is the previous prefix extended by the act at index n of the completed ledger. The two simp lemmas prefix_zero and prefix_succ are immediate reflexivity of these clauses.
why it matters
This cut is the basic interface between infinite ledgers and finite traces in TraceClosure. Downstream, prefix_zero and prefix_succ expose the recursive clauses as simp rules; canonical_prefix_exists uses it to witness that every length-n slice of the canonical completed trace is a nonempty finite Trace.
In the broader Recognition stack, completed traces are the infinite bookkeeping objects behind recognition composition and ledger dynamics. Having a canonical finite-prefix map lets later certificates (traceClosureClaim, TraceClosureCertificate) reason about infinite objects via their finite initial segments without leaving the inductive Trace type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.