orbitTrace

In the primitive recognition calculus, a finite trace is an inductive object: either empty, or obtained by extending a prior trace by one distinction act (K2.4). The distinguished one-step map step always appends the fixed act $\delta$ (R3), so repeated application builds pure $\delta$-chains.

The local module develops the syntactic algebra of traces (append, extends, length) before any metric or cost structure is imposed. Length itself is valued in the RS-native real type used for geometric quantities elsewhere in the stack.

Upstream, successor on natural numbers is the ordinary inductive step; here it indexes how many times $\delta$ is applied. No curvature, J-cost, or spacetime interpretation is required at this layer.

Not a theorem: a recursive definition on Nat. The zero case returns the empty trace. The successor case wraps the previous value in the one-step $\delta$-extension step. No lemmas are invoked; the recursion is the entire content.

This is the canonical pure orbit used to calibrate length against iteration count. Downstream, length_orbitTrace (K2.12 preview) proves by induction that the length of the $n$th orbit equals $n$, so the syntactic length functional is faithful on $\delta$-chains.

In the broader Recognition stack, finite traces are the discrete substrate on which later defect, metric, and stability constructions sit. Having an explicit $n$-fold $\delta$-orbit lets those layers quote a concrete, length-$n$ witness without building ad hoc sequences. It does not yet touch the forcing chain (T5–T8), RCL, or the mass ladder; it is foundation scaffolding for those later geometric readings.