IndisputableMonolith.Foundation.SeamClosure.Reference
Defines referring traces: a subject trace marked against a held ground trace, the delta-native carrier of aboutness. Both subject and ground are ordinary traces, so no new constructor appears. The module builds the refers-to relation, self-reference exclusion, step reference, generated sets, and a small referring algebra. Foundation readers cite it when formalizing reference without extra ontology.
claimA referring trace is a pair of ordinary traces $(S,G)$ where the subject $S$ is distinguished relative to a held ground $G$. Aboutness is the relation "$S$ refers to $G$"; self-reference is excluded; step reference and generated closures are defined from that relation. Reference reduces to distinction data already present in the primitive recognition calculus.
background
Recognition Science treats recognition events as discrete traces in a primitive calculus (imported from PrimitiveRecognitionCalculus.Basic). Distinction is already first-class there: one trace can be marked relative to another without adding a new sort of object.
This module packages that idea as reference. A referring trace holds a subject (what is marked) and a ground (the standing context). Both are ordinary traces. The philosophical load of "aboutness" is carried by the distinction relation alone, not by a separate intentional type.
Sibling structure introduces the refers-to predicate (with decidability), proves self-reference is not refers-to, defines step reference and generated sets, records that reference reduces to distinction, and supplies a thin referring algebra with ground evaluation.
proof idea
This is primarily a definition module. Core objects (referring trace, refers-to, self-reference, step reference, generated, receiving, referring algebra, eval-ground) are introduced as structures, inductive or recursive defs, and Prop-level relations over existing traces.
Lemmas are short: decidability of refers-to, self-reference is not a refers-to instance, generated-all closure facts, and the reduction of reference to distinction. No deep analytic argument; the work is naming and wiring the delta-native carrier so later seam-closure results can quote a single vocabulary.
why it matters in Recognition Science
Seam closure needs a precise stand-in for aboutness that does not smuggle in new ontology. Referring traces supply that stand-in: subject against ground, both ordinary traces, so the forcing chain and recognition composition law stay on the same carrier type.
Downstream pages in Foundation/SeamClosure can cite the refers-to relation, the self-reference exclusion, and the reduction-to-distinction lemma when closing seams or evaluating ground. With no recorded used-by edges yet, the module is infrastructure: it freezes the vocabulary for reference before larger closure theorems are stated.
In the broader RS picture this sits under Foundation, upstream of physics landmarks (T5–T8, RCL, phi), as pure structural setup for how one recognition can be about another.
scope and limits
- Does not derive physical constants, mass ladders, or forcing steps T5–T8.
- Does not introduce a new intentional or semantic type beyond ordinary traces.
- Does not prove full seam-closure theorems; only reference vocabulary and short lemmas.
- Does not claim empirical aboutness; only a formal delta-native carrier.
- Does not depend on Mathlib beyond ambient Lean infrastructure.
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