boundaryIncidenceSum_zero
plain-language theorem explainer
The incidence sum of the zero free singular 1-chain vanishes at every vertex of S¹. Anyone equating boundary coefficients to finite incidence sums over edge support cites this as the Finsupp base case. The proof unfolds the sum definition and simplifies.
Claim. For every singular $0$-simplex $v$ on $S^1$, if $c=0$ is the zero element of the free $\mathbb{Z}$-module on singular $1$-simplices, then the incidence sum of $c$ at $v$ equals $0$.
background
This module lifts path-level winding on the circle to singular simplices of $S^1$ and proves that displacement kills boundaries, the chain-level fact needed for a winding homomorphism on $H_1(S^1;\mathbb{Z})$.
A singular $0$-simplex is a point of the singular simplicial set of $\mathrm{TopCat.sphere},1$. Free singular $1$-chains are the free $\mathbb{Z}$-module on singular $1$-simplices. The incidence sum of a finite free edge-chain $c$ at a vertex $v$ is the support sum $\sum_e n_e\cdot\mathrm{inc}(e,v)$, the explicit finite expression for the boundary coefficient at $v$.
Upstream, that sum is defined precisely so that equating it to the abstract boundary coefficient becomes local finite-support algebra for later support-decreasing graph arguments.
proof idea
Term-mode unfold of the incidence-sum definition, then simp. The zero Finsupp sums to zero, so the weighted incidence contribution at any vertex is $0$. No external lemmas beyond the definition and Finsupp simplification.
why it matters
Base case of the induction proving that every finite free edge-flow has boundary coefficient equal to its incidence sum over support. Downstream, vertexBoundaryCoeff_eq_incidenceSum_holds opens with Finsupp.induction_linear and rewrites the zero branch by this lemma.
That equality is the local finite-support algebra needed for the support-decreasing graph proof in the circle-winding chain development. In the broader module story it sits under the kills-boundaries identity (simplexDisplacement_boundary) and the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ via winding; it does not itself touch T0–T8 or the RCL, but keeps the singular-chain bookkeeping honest for that homology comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.