ratio_induced_zero_iff
plain-language theorem explainer
For any ratio map embedding a configuration space into the positive reals, the induced RS cost vanishes exactly when the configuration's ratio equals 1. Citation target for anyone linking balance of a configuration to zero J-cost in the Physics of Reference. Proof is a one-line reduction to the standard J-cost zero criterion after unfolding the induced cost.
Claim. Let $C$ be a configuration type and $\iota$ a ratio map $C \to \mathbb{R}_{>0}$. For every $c \in C$, the ratio-induced cost satisfies $J_{\iota}(c) = 0$ if and only if $\iota(c) = 1$.
background
The module formalizes the Physics of Reference: aboutness as cost-minimizing compression. A symbol points to an object when the connecting ledger entry minimizes J-cost. The canonical cost is the RS functional $J(x) = \tfrac12(x + 1/x) - 1$ (equivalently $\cosh(\log x) - 1$), forced uniquely by the Recognition Composition Law and the T5 step of the forcing chain.
A ratio map embeds an arbitrary configuration space $C$ into $\mathbb{R}_{>0}$, so the RS cost can be pulled back. The induced cost on $C$ is just $J$ composed with that embedding. Upstream, Jcost_eq_zero_iff already records that $J(x) = 0$ iff $x = 1$ for positive $x$; the present result transports that criterion to configuration space.
proof idea
Unfold the definition of the ratio-induced cost (so the goal becomes $J(\iota(c)) = 0 \leftrightarrow \iota(c) = 1$). Apply the upstream lemma that $J(x) = 0$ iff $x = 1$ for $x > 0$, feeding the positivity certificate that every ratio map carries. Term-mode, no further casework.
why it matters
Zero cost is the mathematical backbone of reference: zero-cost configurations have universal referential capacity, and near-balanced ones can refer to any positive-cost object (effectiveness principle). This iff is the exact bridge from "ratio equals 1" to "induced J vanishes".
It is used immediately by balanced_zero_cost, which states that every balanced configuration (ratio 1 by definition) has zero induced cost. That fact sits under the larger claims that mathematics is the absolute backbone of reference and that representation equivalence is mutual zero reference cost. Within the forcing chain it is local bookkeeping on T5's unique J, not a new forcing step, but without it the ratio-induced reference structure cannot certify balance as zero cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.