verification_equivalence
plain-language theorem explainer
The theorem states that a ledger configuration with N positive ratios is balanced exactly when the sum of J-costs over those ratios equals zero. Recognition Science researchers working on complexity classification would cite this to equate balance verification with a linear scan. The proof unfolds the total cost sum and applies the nonnegativity lemma to reduce the biconditional to per-entry checks via the squared representation of J.
Claim. Let $r_i > 0$ for $i = 1, ..., N$. Then $r_i = 1$ for every $i$ if and only if $J(r_i) = 0$ for every $i$, where $J(x) = (x + x^{-1})/2 - 1$.
background
LedgerConfig N packages a map from Fin N to positive reals together with the positivity proof. The J-cost function obeys J(x) = (x-1)^2/(2x) for x > 0, is nonnegative by the AM-GM inequality, and equals zero precisely at x = 1. The surrounding IC-005 module frames physics complexity via J-cost minimization: ground-state verification reduces to checking that every local ratio equals one, which the module classifies as linear time.
proof idea
Unfolds totalJCost to a sum, rewrites via the lemma that a sum of nonnegative terms vanishes if and only if each term vanishes, then splits the biconditional. One direction substitutes the unit lemma directly. The converse applies the squared-form lemma to each term, cancels the positive denominator, and invokes nonnegativity of squares to force each ratio to one.
why it matters
The result supplies the equivalence used by the downstream ic005_certificate to list ground-state verification as O(N). It realizes the module claim that J-cost minimization is convex with unique minimum at one, thereby placing balance checks in P. The equivalence closes the linear-time verification step in the RS complexity summary without invoking the eight-tick dynamics or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.