composeMorphism
plain-language theorem explainer
Reference morphisms compose: if f never raises reference cost from R₁ to R₂ and g never raises it from R₂ to R₃, then g∘f is a morphism R₁→R₃. Cite this when chaining cost-minimizing compressions in the Algebra of Aboutness. The construction is componentwise map composition plus a two-step ≤ chain on costs.
Claim. Let $R_i$ be reference structures on symbol/object types $(S_i,O_i)$ for $i=1,2,3$. A reference morphism $f:R_1\to R_2$ is a pair of maps on symbols and objects such that $R_2(\mathrm{map}_S s,\mathrm{map}_O o)\le R_1(s,o)$ for all $s,o$ (and likewise for $g:R_2\to R_3$). Then $g\circ f$ is a reference morphism $R_1\to R_3$, with symbol and object maps composed and reference cost non-increasing along the composite.
background
The module formalizes the Physics of Reference: aboutness is ontological compression. A configuration $S$ (symbol) points to $O$ (object) when the ledger link between them minimizes recognition cost. The core object is a reference structure: a nonnegative cost $S\to O\to\mathbb{R}$ measuring how expensive it is for a symbol to refer to an object.
A reference morphism between two such structures is a pair of maps (on symbols and on objects) that preserves the structure in the weak sense that image cost never exceeds source cost. That is the algebraic stand-in for "compression does not get worse under the map." Upstream cost notions in RS (J-cost on ratios, recognition-event cost, rung-coarsened totals) all feed the same nonnegativity and comparison language used here.
Locally this sits among the composition theorems listed in the module thesis: reference structures compose via products and sequences, and morphisms are the structure-preserving arrows for that algebra.
proof idea
Pure definitional construction. Symbol and object components are ordinary function composition $g_S\circ f_S$ and $g_O\circ f_O$. The cost inequality is a two-line calc: apply the codomain morphism's cost_le first (cost in $R_3$ of the fully mapped pair $\le$ cost in $R_2$ of the intermediate pair), then the domain morphism's cost_le (that intermediate cost $\le$ original $R_1$ cost). Transitivity of $\le$ on $\mathbb{R}$ closes it. No external lemmas beyond the morphism fields.
why it matters
Gives the composition law for the category-like structure of reference morphisms inside the Algebra of Aboutness. The module's main results list composition theorems explicitly (alongside the triangle inequality for chained reference and representation equivalence at zero mutual cost). Without this arrow, one cannot stack successive compressions while keeping the cost-nonincrease invariant.
In RS terms this is bookkeeping for cost-minimizing reference, not a new physical constant: it sits under RecognitionForcing (recognition is reference) and LedgerForcing (reference events write ledger entries). No downstream uses are wired yet in the graph, so it is infrastructure for later categorical or multi-stage reference arguments rather than a leaf theorem in the forcing chain (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.