prefix_zero
plain-language theorem explainer
The length-zero finite prefix cut from any completed (infinite) distinction ledger is the empty finite trace. Anyone simplifying prefix extraction or inducting on prefix length cites this simp lemma. The proof is pure definitional equality from the base clause of the prefix recursion.
Claim. For every completed trace $S$ (an infinite ledger of distinction acts), the finite prefix of $S$ of length $0$ equals the empty finite trace.
background
In the Primitive Recognition Calculus, a finite trace is an inductive object: either empty, or obtained by extending a shorter trace by one distinction act (K2.4). A completed trace (K4.13/R9) is instead an infinite ledger, a map from natural numbers to distinction acts; it is a trace-closure object, not a finite $\delta$-only trace.
The finite prefix of length $n$ cuts the first $n$ acts out of that ledger and assembles them into a finite trace. By the recursive definition, the length-zero cut is the empty trace, and the successor clause extends the previous prefix by the act at index $n$. This module sits in the foundation layer that closes finite recognition traces into infinite ledgers.
proof idea
One-line reflexivity. The recursive definition of the finite-prefix map has base case $0 \mapsto$ empty trace, so the stated equality holds by definitional reduction (rfl). No lemmas are applied.
why it matters
This simp lemma anchors the base case of prefix extraction from completed traces. Sibling infrastructure in the same module includes the successor prefix rule, canonical completed traces, and the trace-closure certificate. It supports the K4.13/R9 story in which infinite ledgers of distinction acts are the completed objects and finite traces are their initial segments. The dependency graph records no downstream uses yet; the lemma is local simplification fuel for induction and rewriting around completed traces, not a forcing-chain step (T0–T8) or a physical constant identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.