reference_forced_by_distinction
plain-language theorem explainer
Referring traces are the initial pointed referring algebra: any carrier with a basepoint and two commuting one-step extensions admits a unique structure-preserving map out of referring traces. Cite this for the O1.3 claim that reference is forced by distinction alone, with no second primitive. The proof exhibits the canonical evaluation homomorphism and obtains uniqueness by double induction on subject and ground traces.
Claim. For every pointed referring algebra $A$ on a carrier $X$ (basepoint $z$, subject-step $s_{\mathrm{sub}}$, ground-step $s_{\mathrm{grd}}$, with $s_{\mathrm{sub}}\circ s_{\mathrm{grd}}=s_{\mathrm{grd}}\circ s_{\mathrm{sub}}$), there exists a unique map $h$ from referring traces into $X$ sending the empty self-reference to $z$ and intertwining the two one-act $\delta$-extensions with $s_{\mathrm{sub}}$ and $s_{\mathrm{grd}}$.
background
In the primitive recognition calculus a finite trace is either empty or extended by a single distinction act $\delta$. The one-step operator appends that act. A referring trace is a pair of ordinary traces: a subject (what is marked) held against a ground (the standing context). Genuine reference requires subject and ground to differ; the empty self-reference is the basepoint where both are empty.
A pointed referring algebra on a carrier $X$ supplies a basepoint $z$ (image of that empty self-reference), a subject-extension map, a ground-extension map, and the commutativity law that the two extensions commute. Commutativity is forced: the pair obtained by stepping subject then ground is the same referring trace as stepping ground then subject, so any structure receiving both orders must identify them. This is the exact analogue of a product of two natural-number objects among bi-pointed iterations whose steps commute.
A homomorphism into such an algebra preserves the basepoint and intertwines the two one-act extensions with the algebra's subject and ground maps. The module develops seam closure for reference: aboutness carried only by $\delta$, with no extra constructor.
proof idea
Existence is the canonical evaluation homomorphism induced by the algebra: recurse on the subject coordinate with the subject-step, then on the ground with the ground-step, starting from the basepoint (via ground-only evaluation from a fixed subject base). That map is already known to be a homomorphism.
Uniqueness: take any other homomorphism $h$. Extensionality reduces to equality on each referring pair $\langle s,g\rangle$. Induct on the subject trace, generalizing over the ground. The empty-subject case inducts on the ground: empty ground is the basepoint identity; a ground extension applies the ground-intertwining law, the inner inductive hypothesis, and the definition of evaluation. A subject extension applies the subject-intertwining law, the inductive hypothesis, and reflexivity of evaluation. Only the single act $\delta$ appears.
why it matters
This is O1.3 in the seam-closure development: the forcing, or initial-object, property for reference. Referring traces with empty self-reference as basepoint and the two one-act $\delta$ extensions as steps are initial among pointed referring algebras. That is the precise sense in which reference is forced by distinction: the only act is $\delta$, and the only extra law is the commutativity already forced by two-dimensional generation.
The result is the exact analogue of the trace orbit being the initial pointed iteration in the primitive calculus. It closes the slogan that aboutness needs no second primitive beyond distinction. Downstream use sites are not yet wired in this graph snapshot; the theorem stands as the universal property that any later construction of reference, seam, or aboutness must factor through uniquely.
Within the broader Recognition forcing chain it sits at the foundation layer (pre-T5 cost uniqueness), fixing the carrier of reference before J-cost, $\varphi$, or dimensional forcing are invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.