meaning_compositional
plain-language theorem explainer
Product composition of reference structures preserves meaning: if each symbol is a cost-minimizer for its object, the paired symbol minimizes cost for the paired object under additive product cost. Cited by anyone assembling the Algebra of Aboutness composition layer. The proof is a short tactic that feeds the two minimality hypotheses into additivity of ≤.
Claim. Let $R_1$ and $R_2$ be reference structures on $(S_1,O_1)$ and $(S_2,O_2)$. Write $\mathrm{Meaning}(R,s,o)$ for "$o$ globally minimizes reference cost of $s$ under $R$". If $\mathrm{Meaning}(R_1,s_1,o_1)$ and $\mathrm{Meaning}(R_2,s_2,o_2)$, then $\mathrm{Meaning}(R_1\times R_2,(s_1,s_2),(o_1,o_2))$, where the product structure has cost $R_1(s_1,o_1)+R_2(s_2,o_2)$.
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 J-cost. The core object is a reference structure: a nonnegative cost map $\mathrm{cost}:S\to O\to\mathbb{R}$.
Meaning is the semantic relation induced by that cost: $s$ means $o$ when $o$ is a global minimizer of $\mathrm{cost}(s,\cdot)$. Product reference composes two structures in parallel by adding component costs on the Cartesian product of symbols and of objects, with nonnegativity inherited from the sum of nonnegative terms.
This sits among the module's composition theorems (products and sequences), alongside triangle inequality for chained reference and the ratio-induced structure coming from the RS cost $J(x)=\tfrac12(x+1/x)-1$.
proof idea
Tactic proof. Introduce the two Meaning hypotheses and an arbitrary competitor pair $p'$ in the product object space. Unfold the product reference structure and simplify: product cost is the sum of the two component costs. Apply add_le_add to the two inequalities obtained by specializing each Meaning hypothesis to the corresponding component of $p'$. The sum of the minimal costs is therefore ≤ the product cost of any competitor, which is exactly Meaning in the product structure.
why it matters
Fills item 5 of the module's main results: composition theorems for reference structures. Product composition is the parallel case (sequential reference via a mediator is the companion construction immediately below). It shows that the cost-minimizing account of aboutness is stable under independent pairing of symbol/object systems, so multi-component reference does not need a new semantic primitive.
No downstream dependents are recorded yet; the lemma is infrastructure for building larger reference algebras from smaller ones. In the broader RS picture it sits with LedgerForcing and RecognitionForcing: reference events are ledger entries, and recognition is reference. It does not itself invoke T5–T8 or the RCL identity, but it inherits the nonnegative J-cost discipline those force.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.