rsCostedSpace
plain-language theorem explainer
The canonical Recognition Science costed space on the positive reals packs the standard J-cost into the CostedSpace interface. Anyone building reference structures, ratio maps, or aboutness arguments on RS cost cites this instance. The body is a direct structure packing of Jcost with the AM-GM nonnegativity lemma on positive reals.
Claim. The positive reals $\{x \in \mathbb{R} : x > 0\}$ form a costed space under the Recognition Science cost $J(x) = \frac{1}{2}(x + x^{-1}) - 1$, with $J(x) \ge 0$ for every $x > 0$.
background
The module formalizes the Physics of Reference: aboutness is cost-minimizing compression. A symbol points to an object when the ledger link between them minimizes J-cost. The main objects are costed spaces, reference structures, and ratio-induced reference from the RS cost.
A costed space equips a type $C$ with a cost map $J : C \to \mathbb{R}$ and a proof that costs are nonnegative. This generalizes the RS cost to arbitrary configuration spaces so that reference, meaning, and mathematical backbone can be stated uniformly.
Upstream, $J(x) = (x + x^{-1})/2 - 1$ is the unique RS recognition cost on positive ratios (T5 J-uniqueness / RCL). The lemma $J(x) \ge 0$ for $x > 0$ is AM-GM (equivalently $J(x) = (\sqrt{x} - 1/\sqrt{x})^2/2$). The subtype ${x : \mathbb{R} // 0 < x}$ is the natural carrier for ratio configurations.
proof idea
Definitional structure packing, not a proof. The cost field is $x \mapsto \mathrm{Jcost}(x.val)$ on the positive-real subtype. Nonnegativity is discharged by applying $\mathrm{Jcost_nonneg}$ to the subtype property $0 < x.val$. No further rewriting or case analysis.
why it matters
This is the standard RS instance that the Algebra of Aboutness runs on. Module results such as ratio-induced reference, the reference triangle inequality, representation equivalence, and the effectiveness principle (near-balanced configurations can refer to any positive-cost object) all presuppose a costed space; this supplies the canonical one on $\mathbb{R}_+$.
It ties the reference layer to the forcing chain: J is the T5 unique cost, so reference cost inherits the same functional equation and zero set ($J=1$ only at balance). Downstream graph edges are empty in the current mirror, but sibling definitions (unit costed space, mathematical and near-mathematical spaces, perfect symbols) sit next to it as the comparison and specialization ladder.
No open scaffold: the definition is closed once Jcost and Jcost_nonneg are available from Cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.