mathematical_perfect_compression
plain-language theorem explainer
Zero-cost (mathematical) symbols achieve compression factor exactly 1 against any positive-cost object: perfect referential compression. Cite this when treating the mathematical backbone of the Algebra of Aboutness, or when arguing that abstract structure is a universal, lossless pointer. The proof is a one-line simplification: the mathematical hypothesis sets symbol cost to zero, so the compression ratio collapses to 1.
Claim. Let $S$ and $O$ be types with cost functions $J_S$ and $J_O$ (costed spaces). Suppose $S$ is mathematical: $J_S(x)=0$ for every $x\in S$. Then for any symbol $s\in S$ and any object $o\in O$ with $J_O(o)>0$, the compression factor of $s$ referring to $o$ equals $1$ (perfect compression).
background
This module formalizes the Algebra of Aboutness: reference is ontological compression. A configuration $S$ (symbol) points to $O$ (object) when the connecting ledger entry minimizes $J$-cost. A costed space equips a type with a nonnegative cost $J:C\to\mathbb{R}$, generalizing the RS cost $J(x)=\frac12(x+1/x)-1$.
A space is mathematical when every configuration has zero intrinsic cost. That is the abstract backbone: pure structure with no residual defect. The compression factor measures referential efficiency of a symbol against an object of positive cost (the factor is built so that vanishing symbol cost yields value 1).
Upstream, cost appears in several guises (observer events, multiplicative recognizers, rung-coarsened multisets), all tied to the Recognition Composition Law (d'Alembert form on $\mathbb{R}_+$). Here only the zero-cost specialization is used.
proof idea
One-line tactic proof. Unfold the definition of the compression factor; apply the mathematical hypothesis at the symbol $s$, which forces $J_S(s)=0$; then zero_div and sub_zero reduce the resulting arithmetic expression to $1$. No external lemmas beyond the definitional unfolding and the hypothesis $J_S\equiv 0$.
why it matters
Fills the "mathematical backbone" item in the module's complete reference summary: zero-cost configurations are universal, perfectly efficient referents. It is the sharp endpoint of the effectiveness principle (near-balanced configurations can refer to any positive-cost object); here balance is exact, so compression is exact.
In the broader RS chain this is semantic infrastructure rather than a T0–T8 forcing step: it explains why mathematics (zero $J$) can stand for physical content without residual cost, consistent with existence as defect collapse and with recognition-as-reference. No downstream dependents are recorded yet; the result stands as a closed lemma inside Foundation.Reference for any later composition or morphism theorems that need perfect-compression symbols.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.