ratio_reference_zero_iff
plain-language theorem explainer
The ratio-induced reference cost between a symbol s and object o vanishes if and only if their positive real embeddings agree. Anyone working the Algebra of Aboutness or perfect-reference criteria will cite this biconditional. The proof is a short constructor: unfold the ratio reference, apply J(x)=0 iff x=1 on the positive quotient, and recover equality of ratios.
Claim. Let $S$ and $O$ be types with ratio maps $\iota_S:S\to\mathbb{R}_{>0}$ and $\iota_O:O\to\mathbb{R}_{>0}$. For $s\in S$ and $o\in O$, the ratio-reference cost satisfies $R(s,o)=0$ if and only if $\iota_S(s)=\iota_O(o)$.
background
The module formalizes reference as cost-minimizing compression: a symbol configuration $S$ points to an object configuration $O$ when the ledger link between them minimizes the RS cost $J$. A ratio map embeds a configuration space into the positive reals so that $J$ can be applied directly; every value is strictly positive by construction.
The canonical ratio reference structure sets the pairwise cost to $J(\iota_S(s)/\iota_O(o))$, using the standard Recognition cost $J(x)=\frac12(x+1/x)-1$ (equivalently $\cosh(\log x)-1$). Upstream, $J(1)=0$ and the characterization "$J(x)=0$ with $x>0$ forces $x=1$" are already available from the Cost library. Existence-as-defect-collapse and ledger forcing supply the broader setting in which zero cost means perfect match.
proof idea
Unfold the definition of ratio reference so the cost is literally $J(\iota_S(s)/\iota_O(o))$. Split the biconditional.
Forward: positivity of both ratios gives a positive quotient. Feed $J(\mathrm{quot})=0$ into Jcost_zero_iff_one to conclude the quotient equals $1$, then rewrite via div_eq_one_iff_eq (denominator nonzero) to obtain equal ratios.
Reverse: substitute equal ratios, cancel by div_self on the positive object ratio, and apply Jcost_unit0 ($J(1)=0$).
why it matters
This is the exact zero-cost criterion for the ratio-induced reference structure that the module lists among its main results. Downstream, zero_cost_perfect_reference quotes the forward direction to conclude that vanishing cost yields perfect reference (matched ratios plus zero cost). That feeds the broader forcing story: zero-cost configurations form the mathematical backbone with universal referential capacity, and cost-minimization forces cheap symbols for expensive objects.
In framework terms it sits under the Algebra of Aboutness, tying the T5 $J$-uniqueness cost to the semantic relation "s means o". It does not itself force existence of symbols; it characterizes when an already-built ratio reference is perfect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.