unit_is_mathematical
plain-language theorem explainer
The one-point space carrying the constant-zero cost functional is mathematical: every configuration has intrinsic cost zero. Anyone citing the absolute-backbone theorem or the T5-to-canonical-reference bridge needs this base case. The proof is a one-line reflexivity on the constant-zero definition of the unit cost.
Claim. The trivial costed space on the unit type, with cost $J\equiv 0$ on its unique point, is mathematical: every configuration has intrinsic cost zero.
background
The module formalizes reference as cost-minimizing compression: a symbol points to an object when the connecting ledger entry minimizes J-cost. A costed space pairs a type of configurations with a nonnegative cost functional $J$.
A space is mathematical when every configuration has zero intrinsic cost ($\forall x,, J(x)=0$). That is the formal stand-in for abstract mathematical structure inside the Physics of Reference. The unit costed space is the trivial instance: carrier Unit, cost constantly zero (nonnegativity is reflexivity of $\le$).
Upstream, the same module defines the mathematical and near-mathematical predicates and the unit space itself. Downstream consumers treat this fact as the zero-parameter base case for universal referential capacity.
proof idea
Term-mode one-liner. IsMathematical unfolds to $\forall x,, J(x)=0$ on the unit costed space. The cost is definitionally fun _ => 0, so the goal is 0 = 0 at the unique point; rfl closes it. No lemmas are applied.
why it matters
This is the seed instance for the absolute-backbone theorem: mathematics is the unique zero-parameter maximal compressor for any physical space that has at least one positive-cost object. That theorem quotes this result to exhibit a mathematical space that can host symbols referring into physics, explaining Wigner's unreasonable effectiveness inside RS.
It is also wired into the unified forcing chain: t5_to_canonical_reference_bridge_holds packages unit_is_mathematical as the unit_costed_mathematical field of the T5-to-canonical-reference bridge. T5 forces uniqueness of the J-cost $J(x)=(x+x^{-1})/2-1$; the bridge then lifts that uniqueness to a canonical reference structure whose mathematical backbone begins here.
Without a proved zero-cost carrier, the backbone and bridge statements would be empty existentials.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.