PerfectSymbol
plain-language theorem explainer
A perfect symbol is a symbol–object pair whose reference cost vanishes exactly. Anyone working the Algebra of Aboutness or the mathematical-backbone theorems cites it when zero-cost reference is the hypothesis. It is a structure extension of Symbol by the single equation R.cost(s,o)=0; no proof body.
Claim. Fix costed spaces $(S,J_S)$ and $(O,J_O)$ and a reference structure $R:S\times O\to\mathbb{R}_{\ge 0}$. A perfect symbol is a pair $(s,o)$ that is already a symbol for $R$ (i.e. $s$ means $o$ by minimizing reference cost, and $J_S(s)<J_O(o)$) and moreover satisfies $R(s,o)=0$.
background
The module formalizes reference as cost-minimizing compression: a configuration $s$ points to $o$ when the ledger cost of that link is minimal. A CostedSpace equips a type with a nonnegative intrinsic cost $J$, generalizing the RS cost $J(x)=\frac12(x+1/x)-1$. A ReferenceStructure supplies a nonnegative bivariate cost of “$s$ referring to $o$”.
A Symbol packages a pair $(s,o)$ with two obligations: Meaning (the reference cost is minimal for that object) and compression ($J_S(s)<J_O(o)$). PerfectSymbol sits one layer above: the reference cost itself is required to be exactly zero. That is the sharp case of representational equivalence and of the zero-cost configurations that feed the mathematical-backbone results in the same module.
proof idea
Definitional structure, not a proved theorem. It extends Symbol by a single field perfect : R.cost s o = 0. No tactics, no lemmas applied; inhabitants are built by supplying the Symbol data plus a proof that the reference cost vanishes.
why it matters
Zero reference cost is the algebraic content of “perfect aboutness”: the symbol and object are representationally interchangeable at the ledger level. The module thesis ties this to LawOfExistence (existence as defect collapse to 0) and to RecognitionForcing (recognition is reference). Downstream, the Mathematical Spaces section defines a space as mathematical when every configuration has zero intrinsic cost; perfect symbols are the referential counterpart of that zero-cost ideal and underwrite claims such as mathematics_is_absolute_backbone and RepresentationEquiv. In the broader RS chain this is the reference-side shadow of J-uniqueness (T5) and of defect collapse, not a new forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.