selfReference
plain-language theorem explainer
For any finite trace T, the neutral self-reference is the referring pair with subject and ground both equal to T. That pair is the basepoint of the referring structure: it marks nothing because subject is not distinguished from ground. Anyone citing generation of referring traces, the homomorphism predicate into a referring algebra, or the fact that basepoints do not refer will use this constructor. The body is the pair constructor only.
Claim. For every finite trace $T$, the self-reference of $T$ is the referring trace whose subject is $T$ and whose ground is $T$. Equivalently, it is the ordered pair $(T,T)$ in the space of referring traces.
background
In the primitive recognition calculus, a finite trace is built inductively: empty, or extended by one distinction act. Traces are the raw carriers of successive distinctions; no aboutness is built in yet.
A referring trace is a pair of ordinary traces: a subject (what is marked) and a ground (the standing context it is marked against). The reference relation holds precisely when subject and ground differ; when they coincide, the pair points at nothing. Both components remain ordinary traces, so no new generative primitive is introduced.
This module equips that pair type with a basepoint and two one-act moves (extend subject, extend ground), so that aboutness can be generated from neutral self-references by the single distinction act alone.
proof idea
Definitional constructor only: pack the same trace $T$ into both fields of the referring-trace structure. No lemmas, no tactics, no computation beyond the structure introduction.
why it matters
Self-reference is the base constructor of the generation predicate: every generated referring trace starts from some self-reference and then extends subject or ground by one distinction act. The theorem that every referring pair is generated relies on those basepoints (including the empty self-reference). The homomorphism predicate into a referring algebra requires that the empty self-reference map to the algebra zero, so this definition fixes the unit of the free structure. Immediately downstream, the lemma that a self-reference does not refer records that the basepoint is genuinely neutral. In the seam-closure story this is the delta-native carrier of aboutness with a single generative primitive, not a second ontology of reference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.