sum_nonneg_zero_iff
plain-language theorem explainer
Finite sums of non-negative reals vanish exactly when each term is zero. Recognition Science ledger proofs invoke this equivalence to reduce global balance verification to a single total-cost check. The argument rewrites directly to the Mathlib non-negative sum fact over Finsets and simplifies the membership condition.
Claim. For any natural number $N$ and function $f$ from a finite index set of size $N$ to the reals with $f(i)geq 0$ for every index $i$, the sum of all $f(i)$ equals zero if and only if $f(i)=0$ for every $i$.
background
The module Information.PhysicsComplexityStructure places physics in the complexity hierarchy through J-cost minimization. J-cost is the derived cost of a multiplicative recognizer comparator on positive ratios and is non-negative by construction. Upstream ObserverForcing.cost states that the cost of any recognition event is its J-cost, which satisfies the non-negativity hypothesis used here. LedgerForcing.balanced defines a ledger as balanced precisely when its event list is balanced.
proof idea
The proof is a one-line wrapper that applies Finset.sum_eq_zero_iff_of_nonneg to the supplied non-negativity assumption on $f$ and then simplifies the universal quantifier over the full finite index set.
why it matters
This lemma is invoked by the downstream verification_equivalence theorem (IC-005.11), which equates a configuration being balanced with its total J-cost equaling zero. That theorem realizes the module claim that ground-state verification reduces to an O(N) sum check. The result aligns with the RS complexity summary that ground-state verification lies in P, consistent with local 8-tick dynamics and the phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.