prefix_succ
plain-language theorem explainer
The length-(n+1) finite window cut from a completed (infinite) distinction ledger equals the length-n window extended by the act at step n. Anyone building inductive arguments on prefixes of infinite ledgers cites this as the successor step. The equality is purely definitional (rfl).
Claim. For every completed trace $S$ (an infinite sequence of distinction acts) and every $n \in \mathbb{N}$, the finite prefix of $S$ of length $n+1$ equals $\mathrm{extend}(\mathrm{prefix}(S,n),\, S(n))$, i.e. the length-$n$ prefix extended by the act of $S$ at index $n$.
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 (K4.13/R9) is the corresponding infinite object: a map from naturals to distinction acts, an infinite ledger rather than a finite δ-only path.
The finite-prefix operation cuts a window of exact length n from that ledger, rebuilding a finite Trace by successive extension. The zero-length case is the empty trace; the successor case is the content of this lemma.
The surrounding TraceClosure module packages these cuts so that infinite ledgers can be compared, closed, and related to canonical repeating protocols without leaving the finite-trace API.
proof idea
One-line definitional proof: rfl. The finite-prefix function is defined by recursion on the length so that the successor clause is literally Trace.extend (prefix n) (actAt n). No lemmas are applied; simp can fire the equality by reduction alone.
why it matters
This is the inductive step that lets every argument about completed traces reduce to finite Trace reasoning. Together with the zero-prefix base case it justifies recursion and simp-normalization over infinite ledgers in the TraceClosure layer (K4.13/R9).
Downstream siblings (canonical completed traces that repeat the primitive distinction act, prefix-existence facts, orbit ledgers) rely on this successor identity even when no direct used_by edge is recorded yet. It sits in the foundation stack that feeds the forcing chain's discrete ledger structure (eight-tick octave, distinction acts) without itself invoking J-cost or φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.