boundaryIncidenceSum_single
plain-language theorem explainer
For a free singular 1-chain supported on a single edge e with coefficient n, the incidence-sum boundary coefficient at any vertex v equals n times the incidence coefficient of e at v. Algebraists working the finite-support graph argument for singular H₁(S¹) cite it as the singleton base case. The proof unfolds the sum definition and applies the Finsupp single-index identity, then normalizes.
Claim. Let $e$ be a singular $1$-simplex of $S^1$, $n\in\mathbb{Z}$, and $v$ a singular $0$-simplex. Writing $c$ for the free $\mathbb{Z}$-chain with sole support $e\mapsto n$, the incidence sum of $c$ at $v$ equals $n$ times the incidence coefficient of $e$ at $v$: $\sum_e n_e\,I(e,v)=n\,I(e,v)$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular one-simplex (resp. zero-simplex) is an element of the singular simplicial set of $\mathrm{TopCat.sphere},1$ in degree $1$ (resp. $0$). The free module on those $1$-simplices is the ambient chain group. The incidence coefficient $I(e,v)$ is $+1$ if $v$ is the terminal vertex of $e$, $-1$ if initial, and their algebraic sum if both endpoints coincide.
The incidence sum of a finitely supported free edge-chain $c$ at vertex $v$ is $\sum_e n_e,I(e,v)$. Upstream, that sum is introduced precisely as the local finite-support expression needed for the support-decreasing graph proof that boundary coefficients equal incidence sums.
proof idea
Unfold the definition of the incidence sum (a Finsupp.sum of $n\mapsto n\cdot I(e,v)$). Rewrite by the standard identity that summing a finitely supported function over a singleton Finsupp.single e n returns the value at that point (with the zero-coefficient side goal discharged by ring_nf). The result is exactly $n\cdot I(e,v)$.
why it matters
This is the singleton base case for vertexBoundaryCoeff_eq_incidenceSum_holds, which states that the boundary coefficient of any finite free edge-flow equals the finite incidence sum over its support (proved by Finsupp.induction_linear, using the zero and single cases). That equality is the local finite-support algebra behind the support-decreasing graph argument in the winding-chain development.
In the broader module story it sits under the chain-level "winding kills boundaries" identity (simplexDisplacement_boundary), which together with the fundamental-loop normalization supplies the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The converse generation half still needs a simplicial prism/subdivision operator not yet in Mathlib singular homology; this lemma does not touch that open half.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.