Symbol
plain-language theorem explainer
A symbol is a pair (s, o) where s means o under a reference structure and the intrinsic cost of s is strictly less than that of o. This is the basic carrier type for the Algebra of Aboutness: reference as cost-minimizing compression. Anyone proving forced emergence of reference, composition of symbols, or the mathematical-backbone theorem cites it. The declaration is a pure structure bundling Meaning with a strict compression inequality; no proof obligations beyond field types.
Claim. Fix costed spaces $(S, J_S)$ and $(O, J_O)$ and a reference structure $R$ with nonnegative cost $R(s,o)$. A symbol is a pair $(s,o)\in S\times O$ such that (i) $o$ minimizes reference cost for $s$: $\forall o',\, R(s,o)\le R(s,o')$, and (ii) compression holds: $J_S(s)<J_O(o)$.
background
The module formalizes reference ("aboutness") as ontological compression rather than a primitive. A costed space equips a type $C$ with a nonnegative cost $J:C\to\mathbb{R}$, generalizing the RS cost $J(x)=\frac12(x+1/x)-1$. A reference structure $R$ supplies a nonnegative cost of one configuration pointing to another.
Meaning is the semantic relation: $s$ means $o$ when $o$ is a least-cost target of $s$ under $R$, i.e. $\forall o',, R.\mathrm{cost},s,o\le R.\mathrm{cost},s,o'$. The compression criterion then requires the symbol configuration itself to be strictly cheaper than the object it denotes.
Upstream cost notions (observer J-cost on recognition events, multiplicative-recognizer derived cost, PRC quotient J-cost, rung-coarsen totals) all feed the same nonnegativity and comparison pattern that CostedSpace abstracts.
proof idea
No proof body: this is a structure definition. It packages four fields: configurations $s$ and $o$, a proof that Meaning holds for $(R,s,o)$, and a proof of the strict inequality $J_S(s)<J_O(o)$. Downstream constructions inhabit the type by supplying those witnesses; PerfectSymbol extends it by adding $R.\mathrm{cost},s,o=0$.
why it matters
This is the ontological core of the Physics of Reference: symbols exist because they compress. The existence theorem reference_is_forced (and its forcing-chain wrapper reference_in_forcing_chain) produces a nonempty type of symbols whenever some object has positive cost, tying reference into the T0–T8 chain as a forced consequence of cost asymmetry.
mathematics_is_absolute_backbone uses Symbol to state that zero-cost (mathematical) spaces are universal compressors for any positive-cost physical space, addressing Wigner's effectiveness. PerfectSymbol specializes to zero reference cost; composeSymbols chains symbols through a mediator; symbol_compression_positive extracts a positive compression factor from the strict inequality. RecognitionForcing's slogan "recognition IS reference" lands on this carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.