step
plain-language theorem explainer
One-step extension of a finite recognition trace by the primitive distinction act δ. Anyone building or inducting on traces in the Primitive Recognition Calculus cites this as the atomic growth rule. The body is a one-line application of the Trace inductive constructor.
Claim. Given a finite trace $T$, define $\mathrm{step}(T)$ to be the trace obtained by adjoining one primitive distinction act $\delta$ to $T$.
background
In the Primitive Recognition Calculus, the only object-level act is the distinction $\delta$ (K2.1). A finite trace (K2.4) is the free inductive structure generated by the empty trace and successive extensions by distinction acts: either empty, or $\mathrm{extend}(T,a)$ for a prior trace $T$ and act $a$.
This module packages those primitives and the basic operations on them. The one-step rule R3 is the special case of extension that always adjoins $\delta$, so every length increase is forced by the same primitive act. Downstream composition (append) and the extends relation are built from the same inductive spine.
proof idea
Pure definition: apply the Trace constructor extend to the input trace and the sole DistinctionAct value delta. No lemmas, no tactics.
why it matters
R3 is the atomic clock tick of recognition: every longer trace is obtained by iterating this step. It sits under append, Extends, and the whole PRC stack, and is referenced across action convexity, cost algebra, causality balls, and multiple astrophysics ladder results (nucleosynthesis tiers, pulsar bimodality, tidal locking). In the forcing chain it is the discrete growth step that later meets the eight-tick octave (T7) and the J-cost calculus; without a single canonical one-step, the free monoid of traces would not be pinned to $\delta$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.