IndisputableMonolith.Foundation.SeamClosure.Reference
Defines referring traces: a subject trace marked against a held ground trace, as the delta-native carrier of aboutness. Both subject and ground are ordinary traces, so reference adds no new constructor. The module packages the relation refers-to, self-reference, step reference, generated sets, and a small referring algebra with ground evaluation. Anyone working the seam-closure layer of the primitive recognition calculus would cite it.
claimA referring trace is a pair $(S,G)$ of ordinary traces, with subject $S$ (what is marked) and ground $G$ (the standing context). The relation $\mathrm{refersTo}$ holds when $S$ is distinguished relative to $G$; self-reference and single-step reference are special cases. Generated sets collect traces reachable by iterated reference; evaluation on ground recovers the held context. Reference reduces to distinction: no extra ontological primitive is introduced.
background
The setting is the foundation seam-closure layer, built on the primitive recognition calculus. Traces are the basic delta-native objects of that calculus: finite records of recognition events. Distinction is the primitive act of marking one trace against another.
This module treats aboutness without a new sort. A referring trace is just a subject trace held relative to a ground trace. The subject is "what is marked"; the ground is "the standing context it is marked against". Both remain ordinary traces.
Sibling structure includes the decidable refers-to relation, self-reference (and the fact that pure self-reference does not count as external refers-to), step reference, the generated closure of a seed under reference, a receiving operation, a referring algebra, and ground evaluation.
proof idea
This is largely a definition module. Core objects (referring trace, refers-to, self-reference, step reference, generated sets, referring algebra, ground evaluation) are introduced as structures, inductive predicates, or plain defs on traces from the primitive calculus. Short lemmas discharge immediate consequences: decidability of refers-to, self-reference does not satisfy external refers-to, every generated element arises by iterated reference, and reference reduces to distinction. No deep forcing or analytic argument lives here; the work is packaging and elementary closure facts.
why it matters in Recognition Science
Seam closure needs a carrier for aboutness that stays inside the trace ontology. Referring traces supply that carrier: reference is distinction of a subject against a held ground, not a new constructor. Downstream seam-closure and recognition-composition arguments can therefore talk about "what a mark is about" while remaining delta-native.
The module sits under Foundation and imports only the primitive recognition calculus basic layer. It does not yet appear as a direct depends_on edge of named parent theorems in the supplied graph, but its siblings (reference reduces to distinction, generated closure, referring algebra) are the natural hooks for later seam-closure uniqueness and composition results in the forcing chain neighborhood (T5 J-uniqueness and the recognition composition law live upstream in spirit; this module supplies the referential vocabulary those layers need when marks carry content).
scope and limits
- Does not define J-cost, phi, or the forcing chain T0–T8.
- Does not prove physical constants, mass formulae, or dimensional claims.
- Does not introduce a new ontological constructor beyond ordinary traces.
- Does not by itself establish uniqueness of seam closure or RCL identities.
- Does not supply downstream used_by theorems in the current graph snapshot.
depends on (1)
declarations in this module (18)
-
structure
ReferringTrace -
def
refersTo -
instance
instDecidableRefersTo -
def
selfReference -
theorem
selfReference_not_refers -
def
stepReference -
inductive
Generated -
theorem
generated_all -
theorem
reference_reduces_to_distinction -
structure
receiving -
structure
ReferringAlgebra -
def
evalGround -
def
eval -
theorem
eval_ground_step -
def
IsHom -
def
evalHom -
theorem
evalHom_isHom -
theorem
reference_forced_by_distinction