symbol_transitivity
plain-language theorem explainer
If s is a symbol for an intermediate m and that same m is a symbol for o, sequential reference from s to o costs at most the sum of the two link costs. Cite this when chaining meanings through a mediator space. The proof is a short calc: mediator optimality at the shared intermediate, then rewrite by the matching hypothesis.
Claim. Let $S$, $M$, $O$ carry costed spaces and let $R_1$ (resp. $R_2$) be a reference structure $S\to M$ (resp. $M\to O$), with $M$ nonempty. Suppose $(s,m)$ is a symbol under $R_1$ and $(m',o)$ is a symbol under $R_2$, with $m=m'$. Then the sequential-reference cost satisfies $(R_1\circ_{\mathrm{seq}}R_2)(s,o)\le R_1(s,m)+R_2(m',o)$.
background
The module develops the Algebra of Aboutness: reference as cost-minimizing compression rather than a metaphysical primitive. A costed space equips a type with a nonnegative intrinsic cost $J$. A reference structure assigns a nonnegative cost to one configuration pointing at another. A symbol is a pair $(s,o)$ that both means its object (minimizes reference cost) and compresses it ($J(s)<J(o)$).
Sequential reference composes two structures through a nonempty mediator type $M$: the cost from $s$ to $o$ is $\inf_m\bigl(R_1(s,m)+R_2(m,o)\bigr)$. The module already records a triangle inequality for chained reference; the present result specializes that geometry to actual symbols whose intermediate endpoints coincide.
proof idea
Invoke sequential-mediator optimality at the first symbol's object $m$: the sequential cost from $s$ to $o$ is at most $R_1(s,m)+R_2(m,o)$ for that particular mediator. Rewrite the second summand by the matching hypothesis $m=m'$, so the right-hand side becomes the sum of the two symbols' reference costs. The whole argument is a two-step calc: optimality inequality, then a single rewrite.
why it matters
Among the module's composition theorems, this is the symbol-level chaining bound: if $s$ means $m$ and $m$ means $o$, sequential reference realizes $s$ about $o$ at cost no worse than the sum of the links. That supports the core thesis that aboutness is ontological compression forced by cost minimization, and sits next to the reference triangle inequality and the effectiveness principle for near-balanced configurations. No downstream users are recorded yet; the lemma is available infrastructure for multi-hop meaning chains in the Physics of Reference. It does not itself invoke the RS landmarks (T5 J-uniqueness, $\varphi$, eight-tick), but inherits the same nonnegative cost discipline those landmarks force.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.