ReferenceStructure
plain-language theorem explainer
A reference structure is a non-negative cost of a symbol configuration pointing at an object configuration. It is the primitive of the Algebra of Aboutness: aboutness is cost-minimizing compression, not a metaphysical primitive. Anyone building symbols, morphisms, or effectiveness results cites it. The declaration is a bare structure (cost map plus nonnegativity), not a proved theorem.
Claim. A reference structure on types $S$ (symbols) and $O$ (objects) is a map $\mathrm{cost}: S \times O \to \mathbb{R}$ such that $\mathrm{cost}(s,o) \ge 0$ for all $s \in S$ and $o \in O$. The value $\mathrm{cost}(s,o)$ is the cost of $s$ referring to $o$.
background
The module formalizes the Physics of Reference: one configuration $S$ (symbol) points to another $O$ (object) when the ledger link between them minimizes recognition cost. Existence is defect collapse to zero; recognition events are themselves reference events that write ledger entries.
Upstream cost notions all feed the same idea. Observer forcing takes the cost of a recognition event to be its $J$-cost $J(x)=\frac12(x+1/x)-1$ (non-negative). Multiplicative recognizers induce a derived cost on positive ratios. Cosmology coarsening sums a ratio weight (doubled $J$) over events. The present structure abstracts those concrete costs to an arbitrary non-negative bilocal cost on symbol/object pairs.
Sibling notions in the same file include costed spaces (configurations with an intrinsic $J$), ratio maps into $\mathbb{R}_+$ so that RS $J$ applies directly, symbols, perfect symbols, and mathematical (zero-cost) configurations.
proof idea
No proof body: this is a structure declaration. It packages two fields only: a real-valued cost of symbol-to-object reference, and the axiom that every such cost is non-negative. Instantiations (indicator reference, ratio-induced reference, etc.) discharge nonneg case-by-case, typically by split_ifs and norm_num, or by inheritance from $J \ge 0$.
why it matters
This is the core object of the Algebra of Aboutness. Downstream, classification of reference quality (perfect / effective / weak) thresholds the cost; identity and composition of reference morphisms require a ReferenceStructure on each leg; symbol composition chains two structures through a mediator; the effectiveness principle builds an existential witness that near-balanced symbols can refer to any positive-cost object.
It sits under the module's main claims: reference forced by asymmetry, mathematics as absolute backbone (zero-cost universal referents), ratio-induced reference from RS $J$, the reference triangle inequality, and representation equivalence at mutual cost zero. In the broader forcing chain it is the interface where ledger/recognition cost becomes "aboutness," connecting Law of Existence, Ledger Forcing, and Recognition Forcing without yet forcing $J$-uniqueness (T5) or $\varphi$ (T6) inside the structure itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.