canonical_prefix_exists
plain-language theorem explainer
For every natural number n, the length-n prefix of the canonical completed trace is a finite recognition trace, so finite traces are inhabited. Cite this when moving between infinite completed orbits and finite distinction sequences under trace closure. The proof is a one-line witness: pack the finite-prefix of the canonical completed trace at n.
Claim. For every natural number $n$, the type of finite traces is inhabited: the length-$n$ prefix of the canonical completed trace (the completed trace that repeats the primitive distinction act $\delta$ at every step) is a finite trace.
background
In the Primitive Recognition Calculus, a finite trace is an inductive object: empty, or extended by one distinction act (K2.4). A completed trace is the infinite counterpart, an assignment of a distinction act at every natural-number time. The canonical completed trace is the constant one: it repeats the primitive act $\delta$ at every index.
The finite-prefix operation cuts a completed trace to a genuine finite trace of prescribed length. Trace closure (module setting, K4.13 neighbors) is the bridge from the infinite natural-number side (completed orbit ledgers of $\delta$-orbit positions) to these finite distinction sequences.
This declaration records the elementary non-vacuity fact that every such cut of the canonical object is well-typed as a finite trace.
proof idea
Term-mode one-liner. Evaluate the finite-prefix map of the canonical completed trace at the given $n$, and wrap the resulting finite trace in the Nonempty witness constructor. No auxiliary lemmas are required beyond the definitions of the canonical completed trace and of finite prefix on completed traces.
why it matters
Trace closure links infinite completed orbits to finite recognition traces. Showing that every prefix of the canonical completed trace is a legitimate finite trace is the non-vacuity step on the finite side: concrete finite objects are obtained by cutting the infinite canonical object.
Sibling infrastructure in the same module includes the completed-orbit ledger (K4.13: infinite sequence of finite $\delta$-orbit positions), the natural-number reading of the canonical object, and the trace-closure certificate package. No downstream consumers are wired yet; the lemma is foundation stock for later closure and ledger arguments.
In the broader Recognition Science chain it supports the discrete recognition calculus that underwrites distinction-act bookkeeping (eight-tick octave T7, and the finite traces behind mass and coupling ladders).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.