length
plain-language theorem explainer
Finite-trace length counts distinction acts: empty has length 0, and each one-step extension increments by one. Anyone working in the primitive recognition calculus cites it as the discrete size of a recognition history. The definition is plain structural recursion on the inductive Trace type.
Claim. The length $\ell$ of a finite recognition trace is the number of distinction acts it records: $\ell(\varepsilon)=0$, and if $T$ is extended by one distinction act $\delta$ then $\ell(T\cdot\delta)=\ell(T)+1$.
background
In the primitive recognition calculus, a finite trace is the inductive history of recognition: either empty, or obtained by extending a prior trace by one distinction act (K2.4). Distinction acts are the atomic steps that build the history; traces are the finite sequences of those steps.
Length is the natural-number measure of that history. It is defined by recursion on the two constructors, so it is exactly the count of extensions from the empty trace. The ambient module builds the basic calculus of traces (append, extends, step) before cost and field structure are layered on.
Upstream, successor on natural numbers is the usual Peano generator (one more application of the step). Here that generator is applied once per extension constructor, so length is the Peano height of the trace tree.
proof idea
Not a proof: a definition by structural recursion on Trace. The empty constructor maps to $0$; the extend constructor maps to the successor of the recursive length of the prior trace, ignoring the particular distinction act. No lemmas are invoked; the equations are the definition.
why it matters
Length is the discrete clock and size measure for recognition histories. Downstream it feeds cost algebra (positive domains and finite window lengths for recognition cost systems), astrophysical observability limits (coherence energy and geometry-only mass-to-light derivations), crystal symmetry counts, and ionization-proxy formulas that index by natural size.
In the broader Recognition Science stack, finite traces sit under the forcing chain and the eight-tick octave: counting acts is how discrete period structure and windowed cost become well-typed. Without a canonical length, append-associativity, extends-relations, and any cost that depends on window size would lack a common Nat-valued measure.
It is scaffolding-free infrastructure: a pure definition used by dozens of later declarations rather than a theorem that closes an open forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.