CostedSpace
plain-language theorem explainer
A costed space is a type of configurations equipped with a nonnegative real-valued cost map. It is the ambient data for the Algebra of Aboutness: every reference structure, symbol, and compression factor is built over a pair of costed spaces. The definition simply packages a cost function with the J ≥ 0 axiom already forced in RS.
Claim. A costed space on a type $C$ is a pair $(J,\mathrm{nonneg})$ where $J:C\to\mathbb{R}$ assigns an intrinsic cost to each configuration and $\mathrm{nonneg}$ asserts $J(x)\ge 0$ for all $x\in C$. This generalizes the Recognition Science cost $J$ from positive reals to arbitrary configuration spaces.
background
The module formalizes the Physics of Reference: aboutness is ontological compression. One configuration (a symbol) points to another (an object) when the ledger link between them minimizes cost. The ambient objects of that theory are configuration spaces carrying a cost.
In RS the canonical cost on ratios is $J(x)=\frac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$), forced unique by the Recognition Composition Law and the T5 step of the forcing chain. Nonnegativity of $J$ is a theorem, not an extra axiom. CostedSpace lifts that package off $\mathbb{R}_{>0}$ so the same language applies to symbols, mediators, and objects of any type.
Upstream modules already use specialized costs (recognition-event cost, multiplicative-recognizer derived cost, rung-coarsen multiset cost). This structure is the common interface those notions instantiate when reference is defined abstractly.
proof idea
Definitional structure with no proof body. The two fields are the cost map $J:C\to\mathbb{R}$ and the universal nonnegativity witness $\forall x,,0\le J(x)$. Instantiation elsewhere supplies a concrete $J$ (for example the RS $J$-cost or the zero cost on Unit) and discharges nonnegativity by the corresponding $J\ge 0$ theorem.
why it matters
Every major object in the Algebra of Aboutness is parameterized by costed spaces: ReferenceStructure, Symbol, PerfectSymbol, composeSymbols, and compressionFactor all take CostedSpace arguments. Predicates IsMathematical and IsNearMathematical are defined directly on CostedSpace (zero cost everywhere, or cost below a threshold).
Downstream theorems that cite it include the effectiveness principle (near-balanced configurations can refer to any positive-cost object), mathematical_perfect_compression (mathematical symbols achieve compression factor 1), mathematical_universal_capacity, and mathematics_is_absolute_backbone. Those results turn the RS fact that $J=0$ configurations are free into a universal referential capacity, tying reference theory back to LawOfExistence (existence as defect collapse to 0) and RecognitionForcing (recognition is reference).
Within the forcing chain this is scaffolding for T5-style uniqueness applied off the positive reals: once a space carries a nonnegative cost, the compression and composition theorems become available without re-proving nonnegativity case by case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.