generated_all
plain-language theorem explainer
Every pair of traces forms a referring trace reachable from a self-reference basepoint by finitely many one-act δ extensions of subject or ground. Anyone closing the O1.2 seam (reference reduces to distinction) cites this totality fact. The argument is double induction on the two Trace constructors, discharging each case with the corresponding Generated constructor.
Claim. For all traces $s$ and $g$, the referring trace with subject $s$ and ground $g$ is Generated: it is reachable from some self-reference basepoint by finitely many one-act $\delta$ moves that extend either the subject or the ground by one step.
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). Both components are built from the primitive recognition calculus, so no new carrier type is introduced. The only act available on a trace is DistinctionAct.delta, carried by the one-step constructor of Trace.
The generation predicate Generated says a referring trace is reachable from a self-reference basepoint (subject equal to ground) by finitely many one-act moves: extend the subject by one δ, or extend the ground by one δ. Because δ is the sole constructor of the act type, a trace is determined by its length, and a referring trace by the pair of lengths.
The local setting is the positive half of obligation O1.2: show that reference is δ-native and needs no second generative primitive.
proof idea
Double structural induction on the two traces. Induct on the subject $s$, generalizing over the ground $g$.
When $s$ is empty, induct on $g$: the empty–empty pair is exactly the base constructor applied to the empty trace; each ground extension is discharged by Generated.extendGround on the inductive hypothesis (the act is necessarily δ, so cases on it is immediate).
When $s$ is a one-step extension of $s'$, case-split the act (again only δ) and apply Generated.extendSubject to the inductive hypothesis at the same ground $g$.
No external lemmas are required beyond the three constructors of Generated and the inductive structure of Trace.
why it matters
This is the unconditional engine behind O1.2. The parent theorem reference_reduces_to_distinction simply unpacks a referring trace and invokes generated_all; its doc-comment records that the refersTo hypothesis is retained only to match the obligation wording, while generation already reaches every pair.
In the Recognition framework this closes a seam-level claim: aboutness (reference) does not require a second generative primitive beyond the single distinction act δ. That keeps the forcing chain's primitive layer thin (one act, traces built by length, referring pairs generated by two one-act moves) and blocks any later attempt to smuggle a frame-level second constructor into the foundation.
Downstream, anything that treats referring traces as δ-native carriers of aboutness can quote this totality rather than re-induct.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.