balanced_config_zero_cost
plain-language theorem explainer
The theorem shows that any finite configuration with every ratio fixed at 1 has summed J-cost exactly zero. Researchers classifying Recognition Science models in the complexity zoo cite it to place ground-state verification in P. The proof reduces directly to the unit lemma for J at argument 1 after unfolding the summation.
Claim. For every natural number $N$, the configuration with all ratios equal to 1 satisfies $J(1) + J(1) + ... + J(1) = 0$ ($N$ times).
background
The IC-005 module frames physics complexity through J-cost minimization on ledger states. J-cost is defined by $J(x) = (x + x^{-1})/2 - 1$, which is strictly convex with its global minimum at $x=1$. totalJCost sums the individual J-cost contributions over the support of a witness whose ratios are positive reals. The upstream lemma Jcost_unit0 states that Jcost 1 = 0 by direct substitution into the definition.
proof idea
The proof is a one-line wrapper that unfolds totalJCost and simplifies with the Jcost_unit0 lemma, replacing each term by zero.
why it matters
This supplies the zero-cost ground-state fact required by the rs_complexity_classes summary inside ic005_certificate. It fills the IC-005.10 slot in the module, confirming that balanced-ledger verification is linear-time and belongs to P. The result instantiates the ground-state clause of the RS complexity hierarchy and aligns with the J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.