instDecidableRefersTo
plain-language theorem explainer
Reference is decidable: for any referring trace, whether the subject is distinct from the ground can be settled by a verifier with no appeal to excluded middle. Anyone building the seam-closure referring algebra or checking aboutness of traces would cite this. The proof unfolds the reference predicate to inequality of traces and reuses the derived decidable equality on Trace.
Claim. For every referring trace $r$ (a pair of ordinary traces: subject and ground), the proposition that $r$ genuinely refers—i.e. that its subject is not equal to its ground—is decidable.
background
In the seam-closure reference module, a referring trace is the candidate delta-native carrier of aboutness: a subject trace marked against a held ground trace. Both components are ordinary traces from the primitive recognition calculus; no new constructor is added. The structure derives decidable equality and a printable representation.
Genuine reference is the proposition that subject and ground are not the same trace. A pair that fails to distinguish them points at nothing and is the neutral basepoint of the referring structure (self-reference). The module sits in Foundation and imports the primitive recognition calculus, so Trace already carries a derived DecidableEq instance from Basic.
Obligation O1.1 asks exactly for a constructive decision procedure on that inequality, so later referring-algebra constructions can branch on whether a trace refers without classical logic.
proof idea
One-line constructive wrapper. Unfold the reference predicate to the bare inequality of the two Trace fields. Because ReferringTrace (and Trace) derive decidable equality, Lean already has a Decidable instance for that inequality; inferInstance discharges the goal. No case split or custom decision procedure is written by hand.
why it matters
This closes O1.1 in the seam-closure reference stack: reference must be decidable so the verifier can always settle whether a referring trace genuinely refers. It underwrites the neutral self-reference basepoint and the step-reference and generated-trace constructions that sit beside it in the same module. In the broader Recognition Science foundation, aboutness is meant to be delta-native and checkable; a classical-only decision would break the constructive ledger story that feeds later forcing and continuum bridges. No downstream theorems yet list this instance (used-by is empty), but every decide-style or branching proof on genuine reference will need it. It does not itself force phi, the eight-tick octave, or D = 3; it is pure infrastructure for the referring algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.