fundamental_theorem_of_reference
plain-language theorem explainer
Marks completion of the Algebra of Aboutness module: reference structures arise from J-cost asymmetry, mathematics is the zero-cost backbone, and near-balanced configurations are near-mathematical. Anyone citing the Physics of Reference package would point here as the narrative capstone. The proof is the term `trivial` on `True`; it does not conjoin the five listed properties as Lean hypotheses.
Claim. In the Recognition Science setting formalized by this module, the fundamental theorem of reference holds in the weak sense that $\top$ is true. Narratively this packages: (1) reference structures forced by cost asymmetry; (2) mathematical (zero-cost) spaces as the referential backbone; (3) positive cost for all non-mathematical reference; (4) zero cost for self-reference induced by ratios; (5) near-balanced configurations being near-mathematical.
background
The module develops the Physics of Reference: aboutness is not a primitive but ontological compression. A configuration $S$ (symbol) points to $O$ (object) when the ledger link between them minimizes the RS cost $J$, with the canonical form $J(x)=\frac12(x+1/x)-1$ (equivalently $\cosh(\log x)-1$ from the T5 uniqueness step).
Sibling notions in the file include costed spaces, reference structures, ratio maps, meaning and unique meaning, symbols and perfect symbols, and the predicates for mathematical versus near-mathematical configurations, plus unit and RS costed spaces. Upstream imports tie existence to defect collapse to zero (LawOfExistence), ledger entries to reference events (LedgerForcing), and recognition itself to reference (RecognitionForcing).
The module's stated main results (forced reference from asymmetry, mathematics as absolute backbone, ratio-induced reference, a reference triangle inequality, composition, representation equivalence, and an effectiveness principle for near-balanced states) are the intended content this capstone names.
proof idea
Term-mode one-liner: the goal is True, discharged by trivial. No lemmas are applied; there is no reduction of the five narrative clauses into a conjunction or structure package.
why it matters
Per the doc-comment, this declaration is meant to complete the formalization of the Algebra of Aboutness inside Foundation. It sits at the end of Foundation.Reference after the cost, ledger, and recognition forcing imports, so it functions as a named landmark for the thesis that reference is cost-minimizing compression under the RS $J$-cost (T5/RCL lineage).
There are no recorded downstream used_by edges; nothing in the graph currently consumes this theorem as a lemma. Its value is bibliographic and structural: a single citeable name for the module's core claims, not a load-bearing step in the T0–T8 forcing chain or the mass/alpha derivations. A referee should treat the five enumerated bullets as documentation of sibling results, not as content proved at this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.