SequentialReference
plain-language theorem explainer
Sequential composition of two reference structures through a nonempty mediator space M. The cost of s referring to o is the infimum over mediators m of the sum of the two hop costs. Cited by symbol composition, mediator optimality, and symbol transitivity. The definition is the infimal convolution of the two cost maps, with nonnegativity from Real.iInf_nonneg and additivity of the component bounds.
Claim. Given reference structures $R_1:S\to M$ and $R_2:M\to O$ (nonnegative cost maps) with $M$ nonempty, their sequential composition is the reference structure $R:S\to O$ with $$R(s,o)=\inf_{m\in M}\bigl(R_1(s,m)+R_2(m,o)\bigr).$$
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 cost. The core object is a reference structure: a map $\mathrm{cost}:S\to O\to\mathbb{R}$ together with a proof that every cost is nonnegative.
Sequential reference is the chained case. One hops $S\to M\to O$ and takes the cheapest mediator. This is the composition half of the module's composition theorems (alongside products). Upstream, costs throughout RS are instances of the J-cost $J(x)=\tfrac12(x+1/x)-1$ (or derived comparator costs); here the construction is abstract and only needs nonnegativity of the two input structures.
The nonempty hypothesis on $M$ ensures the infimum is over a nonempty index set, so the real-valued inf is well-posed in the usual Mathlib sense.
proof idea
Definitional construction, not a deep proof. The cost field is set to $\inf_m,R_1(s,m)+R_2(m,o)$. Nonnegativity is a short tactic proof: apply Real.iInf_nonneg, then for each mediator use add_nonneg on $R_1.\mathrm{nonneg}$ and $R_2.\mathrm{nonneg}$. No uniqueness or attainment of the inf is claimed at this stage.
why it matters
This is the sequential arm of the module's Composition Theorems: reference structures compose by products and by sequences. Downstream, sequential_mediator_optimal records that every concrete mediator upper-bounds the sequential cost (the defining property of an inf). composeSymbols builds a composite symbol through a matched mediator object, and symbol_transitivity lifts meaning along a chain: if $s$ means $m$ and $m$ means $o$, then $s$ can mean $o$ under sequential reference with controlled cost.
In the broader RS picture this is the algebraic skeleton for chained recognition events and ledger paths: multi-hop aboutness is still a single reference structure, so triangle-type bounds and effectiveness arguments apply uniformly. It does not itself force $J$, $\varphi$, or the eight-tick octave; those live in the forcing chain. It supplies the composition primitive those later arguments need when reference is multi-stage.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.