symbol_compression_positive
plain-language theorem explainer
A symbol for a positive-cost object has strictly positive compression factor: one minus the ratio of symbol cost to object cost. Cite this when quantifying how much cheaper a referring configuration is than its referent in the Algebra of Aboutness. The proof is a short algebraic reduction from the Symbol compression inequality via division and linear arithmetic.
Claim. Let $S$ and $O$ carry nonnegative cost maps $J_S$ and $J_O$, and let $R$ be a reference structure $S\to O$. If $(s,o)$ is a symbol (so $s$ means $o$ under $R$ and $J_S(s)<J_O(o)$) with $J_O(o)>0$, then the compression factor $1-J_S(s)/J_O(o)$ is strictly positive.
background
The module formalizes the Physics of Reference: aboutness is ontological compression. One configuration (the symbol) points to another (the object) when the ledger link between them minimizes cost. A costed space equips a type with a nonnegative intrinsic cost $J$, generalizing the RS cost. A reference structure supplies a nonnegative pointing cost between symbol and object spaces.
A symbol is a pair $(s,o)$ that both means $o$ (minimizes reference cost) and is strictly cheaper: $J_S(s)<J_O(o)$. The compression factor is defined as $1-J_S(s)/J_O(o)$ whenever $J_O(o)>0$; it measures how much cheaper the symbol is than its referent. The module thesis is that symbols exist because they compress.
proof idea
Term-mode proof. Unfold the compression factor to $1-J_S(s)/J_O(o)$. From the Symbol field $J_S(s)<J_O(o)$ and the hypothesis $J_O(o)>0$, apply div_lt_one to obtain $J_S(s)/J_O(o)<1$. Conclude $0<1-J_S(s)/J_O(o)$ by linarith. No external lemmas beyond the definition and the Symbol compression inequality.
why it matters
This pins the quantitative content of the Symbol compression criterion: every genuine symbol of a positive-cost object achieves a strictly positive compression factor. It sits in the Algebra of Aboutness chain that forces reference from cost asymmetry (reference_is_forced) and treats zero-cost configurations as the mathematical backbone. The next result in the file sharpens the endpoint: mathematical (zero-cost) symbols achieve compression factor 1. No downstream dependents are recorded yet; the lemma is infrastructure for effectiveness and composition theorems that quantify how near-balanced configurations refer to costly objects. It does not invoke the forcing chain T0–T8 or the RCL directly, but inherits the nonnegativity of $J$ from that foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.