mathematics_is_absolute_backbone
plain-language theorem explainer
Any costed physical space that contains at least one positive-cost configuration admits a zero-cost mathematical space together with a reference structure carrying a genuine symbol for that object. The result is the formal backbone claim behind Wigner's effectiveness: mathematics is the unique zero-parameter compressor for physical configurations. Anyone citing the Algebra of Aboutness or the T5 reference bridge will use it. The proof is a direct constructive witness on the unit type.
Claim. For every type $P$ equipped with a cost $J_P : P \to \mathbb{R}$ (nonnegative), if there exists $o \in P$ with $J_P(o) > 0$, then there exist a type $M$, a cost $J_M$ on $M$, and a reference cost $R : M \times P \to \mathbb{R}_{\ge 0}$ such that $J_M \equiv 0$ and some $s \in M$ is a symbol for $o$: $s$ means $o$ under $R$ and $J_M(s) < J_P(o)$.
background
The module formalizes the Physics of Reference: aboutness is cost-minimizing compression. A CostedSpace equips a type with a nonnegative intrinsic cost $J$, generalizing the RS cost. A ReferenceStructure supplies a nonnegative cost of one configuration pointing to another. A Symbol is a pair $(s,o)$ where $s$ means $o$ (minimizes reference cost) and compresses ($J(s) < J(o)$).
A space is Mathematical when every configuration has zero intrinsic cost: the formal stand-in for abstract, parameter-free structure. The module thesis is that reference is forced by asymmetry in cost, and that zero-cost configurations have universal referential capacity.
Upstream cost notions (ledger balance, observer $J$-cost, multiplicative-recognizer derived cost, PRC orbit balance) supply the ambient language of nonnegative recognition cost; this theorem abstracts them into CostedSpace and does not re-derive uniqueness of $J$.
proof idea
Term-mode constructive proof. Introduce the physical space and costed structure, and unpack the hypothesis to a witness $o_c$ with positive cost. Instantiate the mathematical space as the unit type with the unit costed space (all costs zero) and the indicator reference structure keyed at $o_c$. Discharge the two conjuncts by the sibling fact that the unit costed space is mathematical, and by packaging a Symbol whose symbol is the unique unit point, object is $o_c$, meaning is the indicator-meaning lemma, and compression is the strict positivity hypothesis.
why it matters
This is Main Result 2 of the Algebra of Aboutness module: zero-cost configurations have universal referential capacity, and thereby explain Wigner's unreasonable effectiveness as maximal compression rather than mystery. Downstream, UnifiedForcingChain uses it as the canonical mathematical-symbol witness inside t5_to_canonical_reference_bridge_holds: once T5 has forced uniqueness of $J$, the legacy existential reference bridge is recovered from this backbone theorem plus unit mathematicality.
In the forcing chain, T5 is $J$-uniqueness ($J(x)=\frac{x+x^{-1}}{2}-1$). The bridge packages that uniqueness into a canonical reference story; this declaration supplies the existential half (a mathematical space and a symbol exist whenever physics has positive cost). It sits beside reference-is-forced and the effectiveness principle (near-balanced configs refer to any positive-cost object) as the absolute, zero-parameter end of the same compression ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.