boundaryIncidenceSum_eq_zero_of_boundary_zero
plain-language theorem explainer
If a free singular 1-chain on S¹ has vanishing free-module boundary, and vertex boundary coefficients match incidence sums, then the incidence sum at every 0-simplex is zero. Algebraic topologists running the support-decreasing graph argument for the winding invariant cite this bridge. The proof is a short rewrite: apply the incidence formula, unfold the coefficient maps, and use boundary-zero.
Claim. Assume that for free singular $1$-chains the vertex boundary coefficient equals the incidence sum at each vertex. Let $c$ be a free singular $1$-chain on $S^1$ with free boundary $\partial c = 0$. Then for every singular $0$-simplex $v$, the incidence sum of $c$ at $v$ equals $0$.
background
This module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level fact behind the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $0$-simplex is a point of the singular simplicial set of $\mathrm{TopCat.sphere},1$. Free $1$-chains are finite $\mathbb{Z}$-linear combinations of singular $1$-simplices. The free boundary sends each directed edge to terminal $0$-face minus initial $0$-face. The incidence sum at a vertex $v$ is $\sum_e n_e\cdot\mathrm{inc}(e,v)$, the finite-support weighted count of how edges in the chain meet $v$.
The named hypothesis is the local finite-support identity equating the free-module boundary coefficient at $v$ with that incidence sum; the module documents it as the algebra needed for the support-decreasing graph proof.
proof idea
Short tactic proof. Rewrite the goal by the incidence-formula hypothesis so the target becomes the free-module vertex boundary coefficient of $c$ at $v$. Unfold that coefficient (and the underlying vertex-coefficient extractor). The boundary-zero assumption then makes the coefficient the zero functional applied to $c$, which is definitionally $0$; close by rfl.
why it matters
Sits in the CircleWindingChain development that builds a winding homomorphism on $1$-cycles as a left inverse to the fundamental class: the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, with no axioms or sorry. The incidence-sum vanishing for free cycles is the local bookkeeping step before support-decreasing graph arguments.
Its sole recorded consumer is the primed sibling, which drops the formula hypothesis and states unconditionally that every free-boundary-zero flow has zero incidence sum at each vertex. That unconditional form is what downstream cycle-support reasoning wants. Surjectivity of the integer comparison (generation of $H_1$ by the once-around loop) remains open and 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.