composeSymbols
plain-language theorem explainer
Symbols compose across a shared mediator: if s compresses to m and m compresses to o with matching middle configuration, a sequential reference from the outer source space to the outer object space exists and still strictly lowers cost. Cite this when chaining aboutness or building multi-hop reference. The argument is a short calc that glues the two compression inequalities after rewriting the mediator equality.
Claim. Let $S,M,O$ be types with costed spaces $(J_S)$, $(J_M)$, $(J_O)$ and reference structures $R_1$ on $S\times M$ and $R_2$ on $M\times O$. Suppose $s_1\in S$ is a symbol for mediator $m\in M$ under $R_1$ and $s_2\in M$ is a symbol for object $o\in O$ under $R_2$, with $m$ equal to the symbol configuration of the second pair. Then there exists a reference structure on $S\times O$ and configurations $s\in S$, $o'\in O$ such that $J_S(s)<J_O(o')$.
background
This module formalizes the Physics of Reference: aboutness is ontological compression. A configuration is a symbol for an object when it minimizes reference cost and is strictly cheaper than the object it points to.
A costed space equips a type with a nonnegative cost map $J$. A reference structure supplies a nonnegative cost of one configuration pointing to another. A symbol packages a source configuration $s$, an object $o$, a meaning witness (cost-minimizing reference), and the compression inequality $J(s)<J(o)$.
Composition sits among the module's composition theorems (products and sequences). The local setting is sequential chaining through a mediator space $M$, not a product construction. Upstream cost notions (ledger, recognizer, and ratio costs) motivate why $J$ is the right scalar, but the argument here is purely structural on costed spaces.
proof idea
Witness the outer reference structure by the sequential composite of $R_1$ and $R_2$. Take the outer symbol configuration to be the first symbol's source and the outer object to be the second symbol's object. The cost inequality is a three-line calc: first compression gives $J_S(s_1)<J_M(m)$; rewrite the mediator equality so the middle cost matches the second symbol's source; second compression gives $J_M(s_2)<J_O(o)$. Transitivity of $<$ closes the chain. No external lemmas beyond the symbol compression fields and the sequential-reference constructor.
why it matters
Symbol transitivity is the sequential half of the module's composition package: if $s$ means $m$ and $m$ means $o$, then $s$ can mean $o$ under sequential reference with bounded (strictly lower) cost. That keeps multi-hop aboutness inside the cost-minimization story rather than as a separate semantic primitive.
Module-level results on forced reference, the mathematical backbone (zero-cost universal referents), ratio-induced reference from the RS cost $J(x)=\frac12(x+1/x)-1$, and the reference triangle inequality all assume that reference can be chained; this definition supplies the symbol-level witness for that chaining. It aligns with Recognition-as-reference and ledger entries created by reference events. No downstream uses are recorded yet, so it is infrastructure waiting on higher aboutness theorems rather than a leaf citation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.