UniqueMeaning
plain-language theorem explainer
A symbol uniquely means an object when that object is the unique strict minimizer of reference cost. Semantic uniqueness is meaning plus a strict inequality against every other target. Anyone formalizing injective reference, disambiguation, or perfect symbols cites this predicate. The declaration is a pure definition: the conjunction of ordinary meaning with strict cost uniqueness.
Claim. Fix a reference structure $R$ on symbol type $S$ and object type $O$, with nonnegative cost $R(s,o)$. Symbol $s$ uniquely means object $o$ when $o$ is a cost minimizer for $s$ and the minimum is strict: $R(s,o)\le R(s,o')$ for every $o'$, and $R(s,o)<R(s,o')$ whenever $o'\neq o$.
background
The module formalizes the Physics of Reference: aboutness is cost-minimizing compression. A configuration $s$ points to an object $o$ when the ledger cost of that pairing is minimal. The core object is a reference structure: a map $\mathrm{cost}:S\to O\to\mathbb{R}$ that is pointwise nonnegative.
Ordinary meaning is the weak minimizer predicate: $s$ means $o$ when $R(s,o)\le R(s,o')$ for all $o'$. Unique meaning strengthens that to a strict global minimum, so no other object ties or undercuts $o$. Downstream in the same file, a symbol is a meaning pair that also compresses (cheaper than the object itself).
Costs throughout RS are instances of the J-cost $J(x)=\frac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$), forced by the Recognition Composition Law and T5. Ratio maps embed configuration spaces into $\mathbb{R}_+$ so that $J$ supplies a canonical reference structure.
proof idea
Definitional, not a proof. The predicate is the conjunction of Meaning (weak cost minimization over all objects) with the strict inequality $R.cost,s,o < R.cost,s,o'$ for every $o'\neq o$. No lemmas are applied; uniqueness is encoded directly as a Prop.
why it matters
Unique meaning is the semantic backbone of the Algebra of Aboutness. Without strict uniqueness, reference can be ambiguous: several objects can share the same minimal cost. This predicate is what later notions (Symbol, PerfectSymbol, representational equivalence) refine when they demand unambiguous compression.
It sits under the module thesis that reference is forced by cost asymmetry (reference_is_forced) and that near-zero-cost configurations refer universally (effectiveness_principle). In the broader RS chain, cost is J from T5; recognition events and ledger entries inherit that cost, so unique meaning is the semantic reading of a unique cheapest ledger link from symbol to object.
No downstream theorems currently depend on it (used-by is empty). It is infrastructure for the composition and triangle results listed in the module doc, and for any later injectivity or disambiguation theorems about reference maps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.