reference_reduces_to_distinction
plain-language theorem explainer
Any genuine referring trace is generated from self-reference basepoints by finitely many one-act distinction moves on subject or ground. O1.2 of seam closure: aboutness needs no second generative primitive beyond δ. Cite when arguing that reference is δ-native. Proof destructures the pair and applies the total generation lemma (the refers-to hypothesis is unused).
Claim. Let $r$ be a referring trace (a subject trace held against a ground trace). If $r$ genuinely refers, i.e. subject and ground are distinct, then $r$ is generated: it arises from a self-reference basepoint by finitely many one-act distinction extensions of the subject or of the ground. Only the single distinction act $\delta$ appears.
background
In the primitive recognition calculus a trace is a finite word in the single distinction act $\delta$. The one-step map appends one $\delta$ (R3). A referring trace is a pair (subject, ground): the subject is what is marked, the ground is the standing context. Genuine reference means subject $\neq$ ground; a pair that fails this points at nothing.
Generation is the inductive closure of self-reference basepoints under two moves: extend the subject by one $\delta$, or extend the ground by one $\delta$. The inductive predicate records that nothing beyond $\delta$ is used. An upstream totality lemma already shows every referring pair, referring or not, lies in this closure, because a trace is fixed by its length under the unique act.
This module (SeamClosure.Reference) packages aboutness as a $\delta$-native carrier and discharges the obligation that reference introduces no frame-level second primitive.
proof idea
Term-mode, two steps. Destructure the referring trace into its subject and ground components. Apply the totality lemma that every pair of traces is generated from a self-reference basepoint by the two one-act $\delta$ moves. The genuine-reference hypothesis is present only to match the O1.2 obligation statement; it is not used, since generation already covers the whole carrier.
why it matters
Fills O1.2 in the seam-closure chain: reference reduces to distinction. The positive resolution is that aboutness is $\delta$-native; no second generative primitive is required for referring structure. That keeps the foundation aligned with the single-act calculus that later feeds the forcing chain (unique $J$, $\varphi$, eight-tick octave, $D=3$).
Downstream use sites are not yet wired in this graph snapshot (used-by count zero). The lemma still stands as the certified bridge from the referring-trace carrier to pure distinction generation, and as the place that records the stronger unconditional form via the totality lemma. It closes the scaffolding worry that reference might smuggle in an extra constructor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.