length_orbitTrace
plain-language theorem explainer
The length of the nth pure δ-orbit trace equals n. Anyone counting steps in the primitive recognition calculus (finite traces of distinction acts) cites this when the orbit is built by repeated one-step δ-extension. The proof is a short induction on n that unfolds the recursive definitions of orbit trace and step.
Claim. For every natural number $n$, the length of the orbit trace of order $n$ equals $n$: the finite trace obtained by applying the one-step $\delta$-extension exactly $n$ times has length $n$.
background
In the primitive recognition calculus, a finite trace is an inductive object: either empty, or an existing trace extended by one distinction act (K2.4). The one-step operator step is the special case that always extends by the distinguished act δ (R3).
The orbit trace of order $n$ is the pure δ-chain of length $n$: empty at $0$, and step applied to the previous orbit at successors. Length is the matching recursive counter: $0$ on empty, successor on each extension.
This sits in Foundation.PrimitiveRecognitionCalculus.Basic, which builds the syntactic substrate (traces, append, extends) before strength and forcing material. The result is labeled K2.12 preview: length of the nth orbit trace is n.
proof idea
Induction on $n$. Base case $n = 0$: both sides are zero by definition of orbit trace (empty) and length, so rfl closes. Successor case: unfold orbit trace to step of the previous orbit, unfold step to a single extend by δ, then the inductive hypothesis plus the successor clause of length finishes after simp.
why it matters
K2.12 is a bookkeeping identity in the primitive recognition calculus: the pure δ-orbit is the canonical length-$n$ witness. Without it, later arguments that quantify over traces by length, or that identify discrete time ticks with successive distinction acts, cannot equate syntactic length with the orbit index.
No downstream consumers are wired yet in the graph (used_by is empty), so this is infrastructure rather than a forcing-chain step (T0–T8). It still anchors the discrete side of recognition: eight-tick structure and higher period arguments need a faithful length measure on pure orbits before they can talk about period $2^3$ or octave closure. The declaration is fully proved (no sorry), so it is ready for those consumers when they land.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.