exists_negative_of_sum_zero_of_positive
plain-language theorem explainer
If a finite sum of integers vanishes and one summand is strictly positive, some other summand must be strictly negative. Algebraists and anyone building balanced-flow or Kirchhoff-type arguments on finite supports cite this elementary step. The proof is a short contradiction via Finset.single_le_sum and omega.
Claim. Let $s$ be a finite set and $f:s\to\mathbb{Z}$. If $\sum_{x\in s} f(x)=0$ and there exists $a\in s$ with $f(a)>0$, then there exists $b\in s$ with $f(b)<0$.
background
The ambient module lifts path-level winding on $S^1$ to singular $1$-simplices and proves that simplex displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. That identity, with the generator evaluation on the fundamental loop, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Downstream of the homology setup one works with integer-valued singular $1$-chains that are cycles (boundary zero). At a fixed vertex the incident edge contributions form a finite integer family whose sum is zero by the cycle condition. The present lemma is the pure finite-sum fact used to turn a positive contribution into a guaranteed negative contribution on the same support.
No Recognition-specific cost $J$, $\varphi$-ladder, or forcing-chain hypothesis enters; the statement is ordinary integer arithmetic on Finsets.
proof idea
Proof by contradiction. Assume no element of $s$ has negative $f$-value; push_neg yields $\forall x\in s,, f(x)\ge 0$. Apply Finset.single_le_sum with that nonnegativity witness at the known positive index $a$ to obtain $f(a)\le\sum_{x\in s}f(x)$. Combined with $f(a)>0$ this forces the total sum strictly positive, contradicting the hypothesis that the sum is zero. Close with omega.
why it matters
Feeds directly into exists_negative_edgeContribution_at_oriented_terminal, whose doc-comment calls this "the algebraic core of the next-edge existence step": in a balanced flow (cycle chain), a positive edge contribution at an oriented terminal forces a negative contribution at the same vertex, so a sign-selected supported edge can be continued.
That next-edge step is part of the chain-level bookkeeping around the winding homomorphism on $1$-cycles. The module aims at the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ via simplex displacement and the kills-boundaries identity; surjectivity still needs a simplicial prism/subdivision operator Mathlib does not yet supply. This lemma is the elementary integer hinge inside that program, not a physics forcing step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.