Generated
plain-language theorem explainer
Inductive generation predicate on referring traces: reachability from a self-reference basepoint by finitely many one-act extensions of subject or ground. Anyone proving that reference reduces to pure distinction (O1.2) cites it. The constructors are definitional; no separate proof body.
Claim. A referring trace $r=\langle s,g\rangle$ (subject trace $s$ marked against ground trace $g$) is generated when it arises from some self-reference basepoint by a finite sequence of one-act $\delta$-extensions: either replace the subject by its one-step extension, or replace the ground by its one-step extension. The only act used is the primitive distinction act $\delta$.
background
In the primitive recognition calculus, a trace is a finite word built from the single distinction act $\delta$ (the sole constructor of DistinctionAct). One-step extension appends one $\delta$; length is the number of acts. A referring trace pairs a subject trace with a ground trace: the subject is what is marked, the ground is the standing context. Genuine reference requires subject $\neq$ ground.
Self-reference is the degenerate pair $\langle T,T\rangle$. The minimal genuine reference extends the ground once and holds the old ground fixed. The generation predicate packages exactly those two moves (extend subject, extend ground) starting from self-reference basepoints, so no second generative primitive enters.
The local module develops seam-closure for reference: aboutness carried only by $\delta$-native traces, without new constructors.
proof idea
Definitional inductive predicate, not a proved theorem. Three constructors fix the meaning: (i) every self-reference is generated; (ii) if $r$ is generated, so is the pair with subject stepped once; (iii) if $r$ is generated, so is the pair with ground stepped once. Downstream totality (generated_all) proceeds by induction on the two traces' lengths, using that every trace is a finite iterate of step from empty.
why it matters
This is the carrier for obligation O1.2: reference reduces to distinction. Parent theorem reference_reduces_to_distinction states that every genuine referring trace is generated, with $\delta$ the only act; the stronger unconditional form generated_all shows generation reaches every length pair from $\langle\emptyset,\emptyset\rangle$. Together they close the claim that aboutness introduces no second primitive beyond the forcing-chain distinction act (K2.1).
In the Recognition framework this keeps the seam-closure story aligned with the single-act calculus that feeds T5–T8 (J-uniqueness, $\phi$, eight-tick octave, $D=3$). Downstream gravity and measurement modules only touch the name incidentally; the conceptual load sits in Foundation.SeamClosure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.