boundaryIncidenceSum_eq_zero_of_boundary_zero'
plain-language theorem explainer
Every finitely supported free singular 1-chain on S¹ with vanishing free boundary has vanishing incidence sum at every vertex. Downstream next-edge existence for balanced flows cites this as the algebraic balance identity. The proof is a one-line specialization that discharges the incidence-sum formula hypothesis.
Claim. Let $c$ be a finitely supported integer-valued free chain of singular $1$-simplices on $S^1$, and assume the free singular boundary $\partial c=0$. Then for every singular $0$-simplex $v$, the incidence sum $\sum_e n_e\,\iota(e,v)$ equals $0$, where $n_e$ is the coefficient of edge $e$ and $\iota(e,v)\in\{-1,0,1\}$ records whether $v$ is the terminal face, the initial face, or neither.
background
This module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level fact behind a left inverse to the fundamental class in $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A free singular $1$-chain is an element of the free $\mathbb{Z}$-module on continuous maps $\Delta^1\to S^1$. The free boundary sends each directed edge to (terminal $0$-face) minus (initial $0$-face). The incidence sum at a vertex $v$ is the finite sum of edge coefficients times the local incidence $\iota(e,v)\in{-1,0,1}$; it is the explicit combinatorial expression for the boundary coefficient of $c$ at $v$.
The unprimed sibling assumes a named hypothesis that vertex boundary coefficients equal incidence sums. The present statement is the same conclusion after that formula is available as a proved fact.
proof idea
One-line term wrapper. Apply the unprimed theorem boundaryIncidenceSum_eq_zero_of_boundary_zero, supplying the already-proved identity vertexBoundaryCoeff_eq_incidenceSum_holds as the formula hypothesis, together with the given free-boundary-zero assumption and the target vertex. No further rewriting is needed: once boundary coefficients match incidence sums, vanishing of $\partial c$ forces every incidence sum to vanish.
why it matters
This is the balance identity used by exists_negative_edgeContribution_at_oriented_terminal: in a free-boundary-zero flow, a positive edge contribution at a vertex forces a compensating negative contribution at the same vertex. That existence step is the algebraic core of the support-decreasing graph argument on free $1$-cycles.
In the module's larger program, free $1$-cycles carry the winding homomorphism that is left-inverse to the fundamental class (split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$), via simplexDisplacement and the kills-boundaries identity on $2$-simplices. The present lemma is pure finite-support linear algebra on the free boundary, not a topological winding computation, but it is required infrastructure for walking supported edges of balanced chains.
It does not address the still-open generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle), which needs a simplicial prism or subdivision operator Mathlib singular homology does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.