IsBalanced
plain-language theorem explainer
A configuration is balanced when its ratio-map embedding equals 1. Anyone working the Physics of Reference cites this as the zero-cost locus on a configuration space. The body is a one-line propositional abbreviation: ratio equals unity.
Claim. Given a ratio map $\iota$ embedding a configuration space $C$ into the positive reals, a configuration $c \in C$ is balanced when $\iota(c) = 1$.
background
The module formalizes reference as cost-minimizing compression: a symbol points to an object when the connecting ledger entry minimizes J-cost. The RS cost is $J(x) = \tfrac12(x + 1/x) - 1$ (equivalently $\cosh(\log x) - 1$), forced unique by the T5 step of the forcing chain and satisfying the Recognition Composition Law.
A ratio map embeds any configuration space $C$ into $\mathbb{R}_+$ so that $J$ can be evaluated pointwise. All ratios are required positive. Balanced configurations are exactly those sitting at the fixed point of the reciprocal symmetry $x \leftrightarrow 1/x$, where $J$ vanishes.
Upstream cost definitions (observer events, multiplicative recognizers, rung coarsening, PRC bridge) all reduce to this same $J$ on positive ratios; the present predicate isolates the kernel of that cost on an arbitrary configuration space.
proof idea
Definitional abbreviation, not a theorem. The predicate is literally equality of the ratio-map value with $1$. No lemmas are applied; downstream proofs rewrite with this equality (e.g. via the zero-cost characterization of the ratio-induced cost).
why it matters
Feeds balanced_zero_cost, which proves that every balanced configuration has vanishing ratio-induced J-cost. That zero-cost locus is the mathematical backbone of the module: zero-cost configurations have universal referential capacity, and the effectiveness principle says near-balanced configurations ($J \approx 0$) can refer to any positive-cost object.
In the broader RS picture this is the configuration-space avatar of the T5 J-minimum at $x=1$. It underwrites representation equivalence (mutual reference cost zero) and the claim that mathematics is the absolute backbone of reference. Without a crisp balanced predicate, the compression thesis (reference forced by cost minimization) cannot be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.