ReferenceMorphism
plain-language theorem explainer
A reference morphism is a pair of maps (on symbols and on objects) between two reference structures that never increases reference cost. Anyone building the category of aboutness, or composing reference systems, cites this. It is a structure definition: the cost inequality is the sole axiom, with identity and composition supplied immediately downstream.
Claim. Given reference structures $R_1$ on $(S_1,O_1)$ and $R_2$ on $(S_2,O_2)$, a reference morphism consists of maps $f_S:S_1\to S_2$ and $f_O:O_1\to O_2$ such that for all $s\in S_1$ and $o\in O_1$, $R_2(f_S(s),f_O(o))\le R_1(s,o)$.
background
The module formalizes reference as cost-minimizing compression: a symbol configuration $S$ points to an object configuration $O$ when the ledger cost of that pairing is small. A reference structure is exactly a nonnegative cost function $\mathrm{cost}:S\to O\to\mathbb{R}$.
Upstream, recognition and observer costs are instances of the RS $J$-cost $J(x)=\frac12(x+1/x)-1$ (equivalently $\cosh(\log x)-1$), so reference cost is the same family of defects that appear in ledger forcing and recognition forcing. Zero-cost (balanced) configurations are the mathematical backbone; positive cost marks genuine aboutness.
Morphisms are the structure-preserving maps in this algebra: they may compress or preserve cost, never raise it. That matches the core thesis that aboutness is forced by cost minimization rather than postulated.
proof idea
No proof body: this is a structure declaration. The data are two functions (symbol map, object map) plus one inequality axiom requiring that image pairs cost at most as much as source pairs under the respective reference costs. Nonnegativity of costs is inherited from the ambient reference structures, not restated here.
why it matters
This is the arrow type for the algebra of aboutness. Downstream, the identity morphism (identity on symbols and objects, reflexivity of $\le$) and composition of morphisms (chaining maps and transitivity of the cost inequality) are built directly on it, so reference structures form a category-like calculus of cost-nonincreasing maps.
In the module's main results, composition theorems and representation equivalence need a notion of structure-preserving map; this supplies it. It sits under the Physics of Reference program: reference events create ledger entries, recognition is reference, and effectiveness of near-balanced symbols depends on controlled cost. It does not itself invoke T5–T8, but the costs it compares are the same $J$-family forced there.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.