orbitPositionTrace
plain-language theorem explainer
Maps each finite δ-orbit position to the native recognition trace obtained by applying the distinction act that many times from the empty trace. Cost-uniqueness and character-identity arguments cite it as the canonical finite witness for orbit length, avoiding imported verifier naturals as object theory. The body is a two-clause recursion on the orbit inductive type.
Claim. Associate to each finite orbit position $n$ (base-neutral repeated distinction) a finite recognition trace $T(n)$ by $T(0)=\varepsilon$ and $T(n+1)=\mathrm{step}_\delta(T(n))$, i.e. one $\delta$-extension of the previous trace.
background
In the Primitive Recognition Calculus, a finite trace is either empty or obtained by extending a prior trace by one distinction act (K2.4). The one-step operator appends the generator $\delta$ (R3). Independently, DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): zero or successor, with no imported Peano Nat treated as object theory.
The surrounding module develops native cost uniqueness for PRC characters: cost functionals built from ratio-orbit characters must match doubled-trace and d'Alembert structure without smuggling external arithmetic. Orbit positions therefore need a native length witness inside the trace language itself.
Upstream, successor on logic naturals is "one more application of the generator," and trace step is exactly that generator applied in the recognition calculus. This definition is the bridge: orbit depth becomes a concrete $\delta$-trace.
proof idea
Definition by structural recursion on the orbit inductive type. The zero constructor is sent to the empty trace. The successor constructor is sent to one $\delta$-step of the recursively computed trace. No lemmas are invoked; the equations are the definition.
why it matters
This is the canonical finite $\delta$-trace attached to an orbit position inside PRC native cost uniqueness. Downstream lemmas prove left and right additivity extensions (orbitPositionTrace_add_extends_left/right), order comparison via toNat (orbitPositionTrace_extends_of_toNat_le, orbitPositionTrace_comparable), and feed character hypotheses that identity orientation transports along comparable or canonically merged traces (PRCCharacterNonunitIdentityRespectsComparableTrace, PRCCharacterPrimeIdentityRespectsCanonicalAddTrace).
Those character props remove arbitrary common-extension witnesses and force respect for the specific merger $T(p+r)$. In the Recognition stack this keeps arithmetic internal to repeated distinction (forcing-chain style: structure from the generator, not imported counting), which is required before native cost can be identified with the unique J-cost shape later in the uniqueness pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.