refersTo
plain-language theorem explainer
A referring pair of traces genuinely refers exactly when its subject is not identical to its ground; equal components point at nothing. Seam-closure and aboutness arguments cite this as the atomic reference predicate. The body is pure definitional inequality on the two component traces, with no further proof content.
Claim. Let $r=(s,g)$ be a referring pair of finite traces (subject $s$, ground $g$). Then $r$ genuinely refers if and only if $s \neq g$. When $s=g$, the pair is neutral and points at nothing.
background
In the primitive recognition calculus, a finite trace is empty or extended by one distinction act (K2.4). Equality on traces is decidable by derivation. A referring pair packages two ordinary traces: the subject (what is marked) and the ground (the standing context it is marked against). Both live in the same trace type, so no new inductive constructor appears.
The SeamClosure.Reference module treats aboutness as a delta-native relation on such pairs. The local setting is pre-physics foundation: reduce reference to distinction rather than introduce a second generative primitive. Self-pairs (subject equal to ground) are the neutral basepoints that refer to nothing.
Upstream, the trace type and its decidable equality underwrite later verifier obligations (O1.1): whether a pair genuinely refers must be settleable without excluded middle.
proof idea
Not a theorem proof. The predicate is defined by unfolding to inequality of the pair's subject and ground fields. Downstream code treats it as a transparent Prop abbreviation of ≠ on traces. The related decidability instance is intended as a one-line wrapper: unfold the predicate, then inferInstance from derived DecidableEq on traces (or an equivalent Ne-friendly decide).
why it matters
Atomic filter for genuine reference inside seam closure. Parent uses: the neutral self-pair does not refer; every referring pair is generated from empty/empty by one-act delta moves on subject and ground; under the genuine-reference hypothesis, reference reduces to distinction alone (O1.2), with no second generative primitive; and the verifier instance makes the predicate decidable.
Doc-comment intent: a reference that fails to distinguish subject from ground points at nothing. This is foundation scaffolding for aboutness, not a T0–T8 forcing step, J-cost identity, or constants claim. It closes the definitional half of obligation O1.1; the decidability instance is the companion discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.