sequential_mediator_optimal
plain-language theorem explainer
The sequential reference cost from symbol s to object o equals the infimum of two-hop costs over mediators, and is therefore at most the cost through any fixed mediator m. Composition and symbol-transitivity arguments cite this bound. The proof is the standard complete-infimum lower-bound fact, with bounded-below witnessed by nonnegativity of both hop costs.
Claim. Let $R_1$ be a reference structure from $S$ to $M$ and $R_2$ from $M$ to $O$, with $M$ nonempty. For any $s\in S$, $o\in O$, and mediator $m\in M$, the sequential cost satisfies $\inf_{m'}\bigl(R_1(s,m')+R_2(m',o)\bigr)\le R_1(s,m)+R_2(m,o)$.
background
The module formalizes the Physics of Reference: aboutness is cost-minimizing compression. A reference structure on types $S$ and $O$ is a nonnegative cost map $S\to O\to\mathbb{R}$ measuring how expensive it is for a symbol to point at an object. Sequential composition builds a reference structure $S\to O$ from $R_1:S\to M$ and $R_2:M\to O$ by taking, for each pair $(s,o)$, the infimum over mediators $m\in M$ of the sum of hop costs.
Nonnegativity of each hop (the structure field nonneg) makes the summed family bounded below by zero, so the real infimum exists. This sits among the module's composition theorems and next to the reference triangle inequality, which bounds direct reference by chained reference. Upstream cost notions (J-cost on recognition events, multiplicative-recognizer derived costs) supply the same nonnegativity pattern used here.
proof idea
One-step application of the complete-infimum lemma: the sequential cost is defined as $\inf_m(R_1(s,m)+R_2(m,o))$, so it is $\le$ the value at any particular $m$ once the family is shown bounded below. Boundedness below is witnessed by $0$: for any realized sum $R_1(s,m')+R_2(m',o)$, both summands are $\ge 0$ by the reference-structure nonnegativity axioms, hence so is their sum. No further algebraic identity is needed.
why it matters
This is the elementary optimality fact that makes sequential composition usable: the infimal mediator cost is a genuine lower envelope, so any concrete chain is an upper bound. Downstream, symbol_transitivity relies on it: if $s$ means $m$ and $m$ means $o$, sequential reference lets $s$ mean $o$ with cost controlled by the two symbol hops. In the Algebra of Aboutness it underwrites the composition theorems and sits beside the triangle inequality for reference (direct cost bounded by a chain). Within Recognition Science it is structural scaffolding for aboutness as ledger cost-minimization, not a forcing-chain (T0–T8) step; it does not itself invoke J-uniqueness or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.