zero_cost_perfect_reference
plain-language theorem explainer
Zero ratio-induced reference cost between a symbol and an object forces perfect reference: their positive-real embeddings coincide and the cost is zero. Anyone working the Physics of Reference or RepresentationEquiv cites this converse. The proof is a two-field constructor: one direction of the zero-cost iff, plus the given hypothesis.
Claim. Let $\iota_S:S\to\mathbb{R}_{>0}$ and $\iota_O:O\to\mathbb{R}_{>0}$ be ratio embeddings. If the ratio-induced reference cost of $(s,o)$ vanishes, then reference is perfect: $\iota_S(s)=\iota_O(o)$ and that cost is zero.
background
The module formalizes reference as cost-minimizing compression: a symbol $S$ is about an object $O$ when the ledger link between them minimizes $J$-cost. A RatioMap embeds a configuration space into the positive reals so the RS cost $J(x)=\frac12(x+1/x)-1$ applies directly.
The canonical structure ratioReference inherits that $J$-cost on pairs of ratios. Perfect reference is the Prop that the two ratios match and the induced cost is therefore zero. The forward direction (perfect $\Rightarrow$ zero cost) is immediate from the structure; this theorem is the converse.
Upstream, recognition and observer costs are instances of the same $J$-cost on positive ratios (ObserverForcing, RecognizerBridge, MultiplicativeRecognizer). Existence in the companion LawOfExistence module is defect collapse to zero, so zero reference cost is the referential analogue of existence.
proof idea
Tactic proof by constructor on PerfectReference. The ratio_eq field is obtained by applying the forward direction of ratio_reference_zero_iff to the hypothesis that cost is zero. The cost_zero field is exactly that hypothesis. No further algebraic work.
why it matters
Closes the biconditional between vanishing reference cost and perfect reference in the Algebra of Aboutness. Together with the forward lemma it pins the zero set of ratioReference to equal-ratio pairs, which is the backbone for RepresentationEquiv (mutual zero cost) and the effectiveness principle (near-balanced symbols refer to any positive-cost object).
In the module thesis, mathematics is the absolute backbone precisely because zero-cost configurations have universal referential capacity; this theorem is the local criterion that identifies those configurations. It sits under the Recognition Composition Law and T5 $J$-uniqueness: the cost that vanishes is the forced RS $J$. No downstream dependents are recorded yet; the natural consumers are composition and equivalence theorems in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.