canonical
plain-language theorem explainer
The canonical completed trace is the infinite ledger that places the primitive distinction act δ at every natural-number index. It is the default δ-stream for the primitive recognition calculus: orbit ledgers, prefix lemmas, and cost-algebra packaging cite it as the baseline closed trace. The definition is a one-line structure instance, constant in the time argument.
Claim. The canonical completed trace is the map $\mathbb{N}\to\{\delta\}$ sending every index to the primitive distinction act $\delta$. Equivalently, it is the constant infinite ledger of distinction acts with value $\delta$ at each step.
background
In the primitive recognition calculus, a distinction act is the atomic object-level step $\delta$ (K2.1). A completed trace (K4.13/R9) is an infinite ledger: a function from $\mathbb{N}$ into distinction acts. It is a trace-closure object, not a finite $\delta$-only segment.
The module builds finite prefixes, orbit ledgers, and closure certificates on top of that structure. The local setting is the foundation layer that turns repeated distinction into arithmetic and cost data: prefixes cut finite initial segments; the canonical choice is the pure $\delta$-stream against which other traces are compared.
Upstream, DistinctionAct is the one-constructor inductive whose sole value is $\delta$. Other modules reuse the name "canonical" for initial Peano arithmetic and for forced self-similar dressings; here the meaning is strictly the constant completed $\delta$-ledger.
proof idea
Pure definitional construction. Instantiate the completed-trace structure by setting the act-at-time field to the constant function with value the primitive distinction act $\delta$. No lemmas, no tactics, no proof obligations beyond inhabiting the structure.
why it matters
This is the baseline infinite $\delta$-ledger for Recognition Science's primitive calculus. Downstream cost-algebra packaging (canonical cost algebra data, the canonical recognition cost system, uniqueness and nonnegativity facts for defect distance) treats a fixed closed trace as part of the algebraic setup whose cost is the J-functional satisfying the Recognition Composition Law.
In the forcing chain, repeated distinction is the raw material that later yields the eight-tick octave and the unique J-cost $J(x)=(x+x^{-1})/2-1$. Naming one completed trace as canonical lets orbit ledgers, prefix existence, and trace-closure certificates refer to a single default object rather than quantifying over all infinite ledgers.
It does not itself prove closure or uniqueness of cost; it supplies the reference stream those results act on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.