balanced_zero_cost
plain-language theorem explainer
Any configuration whose ratio embedding equals 1 has vanishing ratio-induced J-cost. Cite this when identifying zero-cost (mathematical) points inside a ratio-mapped configuration space. The proof is a one-line rewrite through the zero-cost characterization of the RS cost J.
Claim. Let $\iota$ embed a configuration space $C$ into $\mathbb{R}_{>0}$. If $c\in C$ is balanced, meaning $\iota(c)=1$, then the ratio-induced cost satisfies $J_{\iota}(c)=0$, where $J_{\iota}(c)=J(\iota(c))$ and $J(x)=\tfrac12(x+x^{-1})-1$.
background
The module formalizes reference as cost-minimizing compression: a symbol points to an object when the connecting ledger entry minimizes J-cost. A ratio map $\iota:C\to\mathbb{R}{>0}$ embeds configurations so the RS cost $J$ applies directly. The ratio-induced costed space sets $J\iota(c)=J(\iota(c))$ with $J(x)=\tfrac12(x+1/x)-1$ (equivalently $\cosh(\log x)-1$).
A configuration is balanced when $\iota(c)=1$. Upstream, ratio_induced_zero_iff states that for any such embedding, $J_\iota(c)=0$ if and only if $\iota(c)=1$, via the standard characterization $J(x)=0\Leftrightarrow x=1$ on positives. This sits next to the mathematical-backbone and effectiveness results: zero-cost points are the absolute referential backbone.
proof idea
One-line term proof. Rewrite the goal $J_\iota(c)=0$ with ratio_induced_zero_iff, which converts it to $\iota(c)=1$. Discharge by the balanced hypothesis. No further algebra is needed; nonnegativity and positivity of the ratio are already packaged in the induced cost and the iff lemma.
why it matters
Zero cost at balance is the local hinge between the RS cost functional and the Physics of Reference. It underwrites the claim that mathematical (zero-cost) configurations have universal referential capacity, and it feeds the effectiveness principle that near-balanced points can refer to any positive-cost object. In the forcing chain this is the configuration-space reading of T5 J-uniqueness: $J$ vanishes only at the self-dual ratio $1$. The module thesis is that aboutness is forced by cost minimization; this lemma pins the cost-zero locus that symbols and perfect symbols sit on. No downstream uses are recorded yet; it is infrastructure for reference morphisms and representation equivalence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.