PerfectReference
plain-language theorem explainer
Perfect reference is the proposition that a symbol configuration and an object configuration stand in exact ratio match under their embeddings into the positive reals, which forces the ratio-induced reference cost to vanish. Anyone working the Physics of Reference or representation-equivalence arguments cites this criterion. It is a two-field Prop structure, not a derived theorem: equality of ratios plus the zero-cost witness.
Claim. Fix ratio embeddings $\iota_S:S\to\mathbb{R}_{>0}$ and $\iota_O:O\to\mathbb{R}_{>0}$. Configurations $s\in S$ and $o\in O$ form a perfect reference when $\iota_S(s)=\iota_O(o)$ and the ratio-induced reference cost between them is exactly zero.
background
The module formalizes reference as cost-minimizing compression: a symbol $S$ points to an object $O$ when the ledger link between them minimizes the RS cost $J$. A ratio map embeds any configuration space into the positive reals so that $J$ applies directly; positivity of the embedding is part of the data.
The canonical reference structure is the ratio-induced one built from $J(x)=\frac12(x+1/x)-1$ (equivalently $\cosh(\log x)-1$). Under that structure the reference cost between $s$ and $o$ is the $J$-cost of the ratio of their embeddings. Zero cost is the hallmark of exact match and of representational equivalence elsewhere in the module.
Upstream cost notions (observer events, multiplicative recognizers, PRC quotient cost) all specialize or double this same $J$; the present criterion is the pure ratio-level statement that match implies vanishing cost.
proof idea
No proof body: this is a structure (Prop) with two fields. The first field asserts equality of the two ratio embeddings at the chosen points. The second field asserts that the cost of the ratio-induced reference structure at those points is zero. Downstream lemmas package the two directions of the criterion by projecting the second field or by reconstructing both fields from a zero-cost hypothesis via the ratio-reference zero-cost iff lemma.
why it matters
This is the Perfect Reference Criterion named in the module thesis: aboutness is ontological compression, and perfect aboutness is exact ratio match with vanishing $J$-cost. It feeds the two companion theorems that perfect reference implies zero cost and conversely that zero cost yields a perfect-reference witness.
Those companions sit under the broader results on mathematical backbone (zero-cost configurations have universal referential capacity), representation equivalence (mutual zero reference cost), and the effectiveness principle (near-balanced configurations can refer widely). In the forcing chain this is the local semantic reading of $J$-uniqueness (T5) and of existence as defect collapse to zero: perfect reference is the referential instance of cost zero.
It does not itself force symbols into existence; that is the separate asymmetry theorem. It only names the exact-match endpoint of the cost landscape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.