unitCostedSpace
plain-language theorem explainer
The trivial costed space on the one-point type: every configuration has cost zero. It is the canonical zero-parameter mathematical backbone used by reference-forcing, the absolute-backbone theorem, and the T5-to-canonical-reference bridge. The construction is immediate: constant-zero cost with nonnegativity by reflexivity of ≤.
Claim. The one-point type $\mathbf{1}$ carries a costed-space structure with constant cost $J(\ast)=0$. Nonnegativity holds because $0\le 0$.
background
The module formalizes the Physics of Reference: aboutness is cost-minimizing compression. A configuration $S$ points to $O$ when the ledger link between them minimizes $J$-cost.
A costed space equips a type $C$ with an intrinsic cost $J:C\to\mathbb{R}$ and a proof that costs are nonnegative. This generalizes the RS cost $J(x)=\tfrac12(x+1/x)-1$ to arbitrary configuration spaces. The one-point type is the zero-parameter carrier: a single configuration with no internal structure.
Nonnegativity of the constant-zero map is discharged by reflexivity of the order on reals (via the foundation order lemmas used in the structure fields).
proof idea
Definitional structure instance, not a tactic proof. Set $J$ to the constant map $_\mapsto 0$ on the unit type. Discharge the nonneg field by le_refl at $0$, so $0\le J(\ast)$ holds definitionally. No further lemmas are required.
why it matters
This is the canonical zero-cost carrier for the Algebra of Aboutness. Downstream, unit_is_mathematical records that it is uniformly zero-cost; reference_is_forced and mathematics_is_absolute_backbone use it as the cheap symbol space that can represent any complex (positive-$J$) object space; effectiveness_principle instantiates near-balanced symbols by the same idea.
In the unified forcing chain, the T5-to-canonical-reference bridge fixes the symbol space as Unit with this costed structure and the indicator reference at a chosen complex object, linking J-uniqueness (T5) to the mathematical-backbone and effectiveness theorems. It is the concrete witness that zero-cost configurations have universal referential capacity (Wigner's effectiveness, in RS language).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.