Trace
plain-language theorem explainer
Finite traces are the free inductive sequences of primitive distinction acts: either empty or one act longer. Anyone building the recognition calculus (append, extension order, one-step dynamics) cites this datatype. It is a pure inductive definition with two constructors and no proof obligations.
Claim. A finite trace is an inductive object: either the empty trace, or the extension of a prior trace by a single primitive distinction act $\delta$.
background
In the Primitive Recognition Calculus, the only object-level generator is the distinction act $\delta$ (K2.1). Everything else is built by stacking those acts. A trace records a finite history of such acts: the empty history, or a history grown by one more $\delta$.
This sits at the base of the foundation layer. The companion one-step map simply extends a trace by $\delta$. Downstream, traces are composed by append and ordered by the extension relation ("$U$ is $T$ followed by some suffix"). The module is the syntactic substrate before cost, strength, or forcing theorems appear.
proof idea
No proof: pure inductive definition. Two constructors (empty and extend by a DistinctionAct), with derived decidable equality and a printable representation. All later lemmas induct on this structure.
why it matters
Traces are the carrier for the entire primitive calculus. Append, its monoid laws (associativity, empty units), the one-step extension, and the Extends preorder are all defined or proved by recursion or induction on this type. Roughly forty downstream uses hang off it in-module alone.
In Recognition Science terms this is the discrete history type before continuous structure (J-cost, $\phi$-ladder, eight-tick octave) is imposed. K2.4 fixes the syntax of recognition sequences; later chain steps reason about cost and forcing on top of these histories.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.