selfReference_not_refers
plain-language theorem explainer
For any finite trace T, the self-reference basepoint built from T fails the genuine-reference predicate: it refers to nothing. Seam-closure and O1.2 arguments cite this as the base case that separates empty self-reference from minimal genuine reference. The proof is definitional: unfold refersTo and selfReference, then simp.
Claim. For every finite trace $T$, the self-reference basepoint associated to $T$ does not genuinely refer: $\neg\,\mathrm{refers}(\mathrm{selfRef}(T))$.
background
In the primitive recognition calculus, a finite trace is either empty or obtained by extending a prior trace by one distinction act (K2.4). The one-step extension by the Kronecker/distinction act $\delta$ is the basic generative move (R3).
This module develops seam-closure reference: when a referring structure built from a trace counts as genuine reference versus a mere basepoint. The predicate "genuinely refers" is the decidable property refersTo on referring traces; selfReference T is the basepoint construction attached to $T$.
The neighboring construction (one-step reference) distinguishes the one-step extension of the ground from the ground itself and is the minimal genuine reference. O1.2 claims every genuine reference arises from basepoints by that construction plus trace extension, with $\delta$ the only act.
proof idea
Purely definitional. Unfold the genuine-reference predicate and the self-reference constructor, then simp discharges $\neg,\mathrm{refers}(\mathrm{selfRef}(T))$ from the unfolded clauses. No external lemmas are required beyond the definitions in this module.
why it matters
Pins the base case of the reference hierarchy in seam closure: self-reference is not genuine reference. That contrast is what makes the one-step reference construction the minimal genuine act, and it is the starting point for the O1.2 generation claim (every genuine reference reachable from basepoints by step-reference and trace extension with $\delta$ only).
No downstream theorems currently depend on this declaration in the graph, so it functions as a local sanity fact and a named lemma for later seam-closure or referring-algebra developments. It sits in Foundation, upstream of mass/ladder physics, and does not itself invoke J-uniqueness, $\varphi$, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.