stepReference
plain-language theorem explainer
Given any ground trace, form the minimal genuine reference by marking its one-step delta-extension against the ground itself. Citation target for the O1.2 generation story: every genuine reference is reachable from self-reference basepoints by this one-act step plus ordinary trace extension. The definition is a one-line structure pair, subject = step(ground) and ground unchanged.
Claim. For any ground trace $g$, the one-step reference is the referring pair $(\mathrm{step}(g), g)$: the subject is the one-act extension of $g$ by the distinction act $\delta$, and the ground is $g$ itself. This is the minimal genuine reference (subject distinguished from ground).
background
In the SeamClosure reference module, a referring trace is a pair of ordinary traces: a subject (what is marked) and a ground (the standing context it is marked against). No new constructor is added; aboutness is carried by distinguishing subject from ground. The reference relation holds precisely when subject and ground are not the same trace; a pair that fails to distinguish points at nothing.
Traces are extended by a single generative primitive, the distinction act $\delta$, packaged as Trace.step. The surrounding generation story (O1.2) says every genuine reference is reachable from self-reference basepoints by finitely many one-act moves: extend the subject by one $\delta$, or extend the ground by one $\delta$. Only that act appears, so no second generative primitive is smuggled in.
Local setting is foundation-level seam closure: reference reduced to distinction on the existing trace calculus imported from PrimitiveRecognitionCalculus.
proof idea
Pure definition, not a proof. The body is the structure constructor for a referring trace: subject is the one-step extension of the supplied ground, and the ground field is that same ground unchanged. No lemmas are applied; it is the canonical pair that witnesses "distinguish the one-step extension from the ground itself."
why it matters
This is the atomic generator for genuine reference in the O1.2 claim: every genuine reference is reachable from basepoints by this construction together with trace extension, with delta the only act. Sibling material builds the generation predicate on referring traces from self-reference basepoints by finitely many subject-step or ground-step moves; this definition is exactly the one-act subject step off a fixed ground.
It keeps the referring algebra delta-native: aboutness is ordinary distinction of traces, not a second primitive. Downstream generation and reduction-to-distinction results in the same module are meant to close the loop that reference introduces nothing beyond the existing recognition calculus. No external used-by edges are recorded yet; the declaration is infrastructure for that local generation story rather than a leaf theorem in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.