144private lemma sum_nonneg_zero_iff {N : ℕ} (f : Fin N → ℝ) 145 (hnn : ∀ i, 0 ≤ f i) : 146 ∑ i : Fin N, f i = 0 ↔ ∀ i : Fin N, f i = 0 := by
proof body
Term-mode proof.
147 rw [Finset.sum_eq_zero_iff_of_nonneg (fun i _ => hnn i)] 148 simp [Finset.mem_univ] 149 150/-- **THEOREM IC-005.11**: A configuration is balanced iff its total J-cost is zero. 151 This means balance verification is equivalent to a single sum = 0 check, 152 which is O(N) in the number of ledger entries. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.