length_empty
plain-language theorem explainer
The empty finite recognition trace has length zero. Anyone simplifying length computations on traces in the primitive recognition calculus will hit this simp lemma. The proof is pure definitional equality: length is defined by recursion with base case 0 on the empty constructor.
Claim. If $T$ is the empty finite trace, then $\mathrm{length}(T) = 0$.
background
In the primitive recognition calculus, a finite trace records a sequence of distinction acts. The inductive type has two constructors: the empty trace, and extension of an existing trace by one distinction act (K2.4).
Length is the natural-number measure of how many distinction acts appear in a trace. By definition it sends the empty constructor to 0 and each extension to the successor of the length of the prior trace.
This module builds the basic algebraic layer (append, extends, length) on those constructors before any continuum or cost structure is introduced.
proof idea
One-line definitional proof. Unfolding length on the empty constructor yields 0 by the first equation of the recursive definition, so rfl closes the goal. Marked @[simp] so the simplifier rewrites empty-trace lengths automatically.
why it matters
Base case for every length argument on finite traces in the primitive recognition calculus. Downstream append lemmas (append_empty, empty_append, associativity) and any induction on trace structure rely on length behaving correctly at the empty seed. No parent theorem currently lists this declaration as a direct dependency, but it is the standard simp fact that keeps length goals from stalling at the empty constructor. It sits at the combinatorial foundation beneath the forcing chain (T0–T8), not yet at J-cost or phi-ladder content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.