ProductReference
plain-language theorem explainer
Parallel product of two reference structures: the cost of a paired symbol referring to a paired object is the sum of the component reference costs. Anyone proving that meaning (zero-cost reference) is stable under independent combination cites this constructor. The body is a two-field structure instance: additive cost plus nonnegativity from sum of nonnegative reals.
Claim. Given reference structures $R_1$ on $(S_1,O_1)$ and $R_2$ on $(S_2,O_2)$, their product is the reference structure on $(S_1\times S_2,\,O_1\times O_2)$ with cost $\mathrm{cost}((s_1,s_2),(o_1,o_2))=R_1.\mathrm{cost}(s_1,o_1)+R_2.\mathrm{cost}(s_2,o_2)$, which is nonnegative whenever both summands are.
background
The module formalizes the Physics of Reference: aboutness is cost-minimizing compression. A symbol configuration $S$ points to an object configuration $O$ when the ledger link between them minimizes recognition cost. The core object is a reference structure: a pair of types $(S,O)$ equipped with a cost map $S\to O\to\mathbb{R}$ that is pointwise nonnegative.
Composition is listed among the main results (products and sequences). Upstream cost notions in the stack (J-cost on recognition events, derived costs of multiplicative recognizers, rung-coarsened multiset costs) all feed the same nonnegativity discipline; here only the abstract structure fields are needed. The product is the parallel (independent) combination of two such costed pointing relations.
proof idea
Definitional construction, not a tactic proof. Set the product cost to the sum of the two projected costs. Discharge nonnegativity by add_nonneg applied to the two component nonneg fields. No further lemmas.
why it matters
Fills the product half of the module's composition theorems. Immediate consumer is meaning_compositional: if each factor has zero reference cost (meaning), the paired symbol has zero product cost, so meaning is preserved under independent combination. That is the algebraic backbone for treating multi-factor symbols and objects without inventing a new cost calculus. In the broader RS picture it keeps reference compatible with ledger additivity and with the forcing chain's cost infrastructure, without yet invoking J-uniqueness, $\phi$, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.