ratioReference
plain-language theorem explainer
Canonical reference structure on symbol and object spaces: the cost of s pointing to o is the RS mismatch cost J of the ratio of their positive embeddings. Anyone working the Algebra of Aboutness cites this as the central construction (reference cost equals J-mismatch). The definition just packages Jcost with nonnegativity from AM-GM on the positive quotient.
Claim. Given ratio embeddings $r_S:S\to\mathbb{R}_{+}$ and $r_O:O\to\mathbb{R}_{+}$, the ratio-induced reference structure has cost $R(s,o)=J\bigl(r_S(s)/r_O(o)\bigr)$ where $J(x)=\frac{x+x^{-1}}{2}-1$, and $R(s,o)\ge 0$ for all $s,o$.
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 connecting ledger entry minimizes recognition cost. The core object is a reference structure: a nonnegative cost $R:S\times O\to\mathbb{R}$.
A ratio map embeds a configuration space into $\mathbb{R}_{+}$, so the unique RS cost $J$ can act directly. Upstream, $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$) is the T5-forced recognition cost, and $J(x)\ge 0$ for $x>0$ by AM-GM.
This definition is listed among the module's main results as the canonical reference structure inherited from that $J$.
proof idea
Definitional construction, not a proof. The cost field is $J$ of the positive quotient of the two ratio embeddings. Nonnegativity is discharged by applying Jcost_nonneg to that quotient, whose positivity follows from the ratio-map positivity hypotheses and div_pos.
why it matters
Module doc calls this the central construction: reference cost equals mismatch cost under $J$. It is the concrete carrier for the Algebra of Aboutness and sits on the T5 J-uniqueness landmark ($J(x)=\frac{x+x^{-1}}{2}-1$).
Downstream it feeds PerfectReference (zero cost iff ratios match), the zero-cost characterization, swap symmetry, self-reference cost zero, the reverse triangle inequality for chained ratios, and the reference complete summary. Those results turn the definition into the backbone for representation equivalence and the effectiveness principle (near-balanced configurations can refer widely).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.