IsMathematical
plain-language theorem explainer
A costed configuration space is mathematical when every configuration has intrinsic cost exactly zero. This is the predicate that isolates zero-parameter abstract structure inside the Algebra of Aboutness. Downstream theorems cite it to prove perfect compression, universal referential capacity, and that mathematics is the absolute backbone of reference. The body is a one-line universal quantification over the cost function of a CostedSpace.
Claim. A costed space $(C,J)$ is mathematical when $J(x)=0$ for every configuration $x\in C$.
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 intrinsic cost. The main thesis is that reference is forced once complex ($J>0$) objects exist, and that zero-cost structure is the universal compressor.
A CostedSpace equips a type $C$ with a cost $J:C\to\mathbb{R}$ that is pointwise nonnegative. This generalizes the RS cost $J(x)=\frac12(x+1/x)-1$ (equivalently $\cosh(\log x)-1$) from the forcing chain to arbitrary configuration spaces. The present predicate singles out the degenerate case in which every configuration is free.
In the module's language, mathematical spaces are the backbone against which physical (positive-cost) objects are referred. The companion notion Near-Mathematical relaxes exact zero cost to a uniform threshold; the exact-zero case is the ideal limit used by the backbone theorems.
proof idea
Definitional, not a proof. The predicate is the Prop $\forall x,, CS.J, x = 0$ on a CostedSpace. Instantiation is by supplying a costed space and discharging the universal (often by rfl when $J$ is constantly zero, as for the unit costed space).
why it matters
This predicate is the hinge of the Mathematical Backbone results in the Algebra of Aboutness. It is the hypothesis of mathematical_perfect_compression (compression factor exactly 1), mathematical_universal_capacity (every positive-cost object is in the referential capacity once meanings exist), and mathematics_is_absolute_backbone (existence of a zero-parameter mathematical symbol space for any complex physical space). The unit costed space is proved mathematical, giving a concrete witness.
In the unified forcing chain it appears in the T5-to-canonical-reference bridge: after T5 forces uniqueness of $J$, the bridge records that the Unit costed space is mathematical and serves as the canonical zero-parameter backbone for reference forcing. That links the cost uniqueness landmark (T5) to the claim that mathematics is the absolute compressor of physical configurations, the formal reading of Wigner's unreasonable effectiveness inside RS.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.