compressionFactor
plain-language theorem explainer
Defines the compression factor of a configuration s relative to a positive-cost referent o as one minus the ratio of their costs. Anyone working the Algebra of Aboutness cites it when quantifying how much cheaper a symbol is than what it points to. The body is a one-line arithmetic definition on two costed spaces.
Claim. Given costed spaces $(S,J_S)$ and $(O,J_O)$ and configurations $s\in S$, $o\in O$ with $J_O(o)>0$, the compression factor is $1 - J_S(s)/J_O(o)$.
background
The module formalizes reference as cost-minimizing compression: a symbol configuration points to an object when the ledger link between them is cheaper than naming the object outright. A costed space equips a type with a nonnegative cost map $J$, generalizing the RS cost $J(x)=\frac12(x+1/x)-1$ to arbitrary configuration spaces.
Compression is the quantitative content of that thesis. If the symbol costs less than the object, the factor is positive and measures fractional savings; if the symbol is free ($J=0$), the factor is exactly one. The positivity hypothesis on the object cost keeps the ratio well-defined and matches the module's standing convention that nontrivial referents have $J>0$.
proof idea
Pure definition: return $1 - J_S(s)/J_O(o)$. No lemmas, no tactics. Downstream proofs unfold it with simp only [compressionFactor] and then use either vanishing of mathematical cost or the symbol compression inequality.
why it matters
This is the scalar that turns the qualitative Symbol predicate into a number. It feeds symbol_compression_positive (every genuine symbol has strictly positive factor) and mathematical_perfect_compression (zero-cost mathematical configurations achieve factor exactly 1). Those results sit under the module's backbone claims: reference is forced by cost asymmetry, and zero-cost configurations have universal referential capacity. In RS terms it is the local bookkeeping for "aboutness" as ontological compression, not a new dynamical law; it does not itself invoke T5–T8 or the RCL, but it is the measure used when those structures are read as reference events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.