ReferringTrace
plain-language theorem explainer
A referring trace is an ordered pair of ordinary finite traces: a subject (what is marked) and a ground (the standing context). It is the delta-native carrier of aboutness in seam closure: reference is just distinction of subject from ground, with no new generative primitive. Downstream work cites it for the reference relation, generation by one-act δ moves, and the initial-algebra forcing theorem that reference is forced by distinction.
Claim. A referring trace is a pair $(s,g)$ where $s$ (subject) and $g$ (ground) are finite traces. Both components are ordinary traces built from the empty trace by successive distinction acts; no extra constructor is added. The intended reading is that $s$ is what is marked and $g$ is the context it is marked against.
background
In the primitive recognition calculus, a finite trace is either empty or obtained by extending a prior trace by one distinction act (the single generative step δ). Traces therefore record finite histories of distinction and carry decidable equality.
Seam closure studies reference (aboutness) without a second primitive. The module treats a referring object as two traces held together: the subject is the marked content; the ground is the standing context. Genuine reference will later mean subject ≠ ground; self-reference (subject = ground) is the neutral basepoint that points at nothing.
This sits under the foundation forcing chain (ledger floor through T8: J-uniqueness, φ, eight-tick octave, D = 3). Here the local task is narrower: package aboutness as a pair of traces so generation, decidability, and initial-algebra uniqueness can be stated purely in terms of δ.
proof idea
Not a theorem: a two-field structure definition. Fields are subject and ground, each of type Trace. The declaration derives DecidableEq and Repr from the corresponding instances on traces. No proof body; mathematical content is the pairing itself plus the doc-stated reading (subject marked against ground).
why it matters
This is the carrier type for the whole Reference submodule. Downstream, refersTo is subject ≠ ground; Generated reaches every pair from self-reference basepoints by extending subject or ground one δ at a time; generated_all shows every referring trace arises that way. The algebra layer (ReferringAlgebra, IsHom, evalHom) and the proved forcing result reference_forced_by_distinction treat referring traces as the initial pointed referring algebra: unique structure-preserving map out of the empty self-reference and the two one-act extensions.
Framework role: O1-style seam closure. Reference is forced by distinction alone (analogue of the trace orbit as initial pointed iteration). No second generative act appears; only δ via Trace.step. That keeps aboutness inside the same primitive used in the T0–T8 chain rather than smuggling in an external semantics of "meaning."
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.