canonical_actAt
plain-language theorem explainer
At every discrete time index the canonical completed trace fires the primitive distinction act δ. Workers in the primitive recognition calculus (trace closure, completed orbits, ledger constructions) cite this as the pointwise content of canonicity. The proof is pure definitional reflexivity from the constant-δ construction of the canonical trace.
Claim. For every natural number $n$, the action of the canonical completed trace at step $n$ equals the primitive distinction act $\delta$.
background
In the primitive recognition calculus, a distinction act is the atomic object-level operation. The inductive type of distinction acts has a single constructor $\delta$ (K2.1): the primitive distinction. A completed trace is an infinite schedule of such acts, recorded as a map from $\mathbb{N}$ into distinction acts.
The canonical completed trace is the constant schedule that returns $\delta$ at every index. That is the local content of canonicity in this module: the free, structureless infinite repetition of the primitive act, before any orbit, strength, or ledger decoration is imposed.
Sibling material in the same file builds finite prefixes of that schedule and packages them into certificates of trace closure. Upstream, $\delta$ is the sole generator of the distinction-act type; the present lemma simply exposes the pointwise evaluation of the canonical schedule.
proof idea
One-line definitional proof. The canonical completed trace is defined by actAt := fun _ => DistinctionAct.delta, so evaluating at any $n$ is definitionally $\delta$. The tactic is rfl; the declaration is marked @[simp] so downstream rewrites discharge the equality automatically.
why it matters
This is the pointwise unfolding lemma for the canonical completed trace in the TraceClosure layer of the primitive recognition calculus. It makes the constant-$\delta$ schedule available to simp, so later constructions (finite prefixes, orbit ledgers, closure certificates in the same module) can treat "act at $n$" as $\delta$ without unfolding the structure field by hand.
No downstream dependents are recorded yet; the lemma is infrastructure for the closure claim and certificate siblings rather than a bridge into the T0–T8 forcing chain. It sits at the object level of recognition (the atomic act $\delta$), not at the level of the J-cost, $\varphi$-ladder, or dimensional forcing. Its role is local hygiene: keep the canonical schedule transparent wherever completed traces are manipulated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.