boundaryIncidenceSum
plain-language theorem explainer
Integer incidence sum of a free singular 1-chain at a vertex on S¹: sum over edges of coefficient times incidence (+1 terminal, −1 initial). Anyone equating vertex boundary coefficients to this sum, or showing boundary-zero flows vanish at vertices, cites it. Defined directly as a finite Finsupp sum against incidence coefficients.
Claim. For a free singular $1$-chain $c$ on $S^1$ (finite integer combination of singular $1$-simplices) and a singular $0$-simplex $v$, the boundary incidence sum is $\sum_e n_e\, I(e,v)\in\mathbb{Z}$, where $n_e$ is the coefficient of edge $e$ in $c$ and $I(e,v)$ is the incidence coefficient: $+1$ if $v$ is the terminal vertex of $e$, $-1$ if initial, and their algebraic sum if both endpoints coincide.
background
The module lifts path-level winding on the circle to singular simplices of $S^1$ and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $0$-simplex is a point of $S^1$ in the singular simplicial set. Free singular $1$-chains are the free $\mathbb{Z}$-module on singular $1$-simplices. The incidence coefficient of a directed singular edge at a vertex is $+1$ at the terminal vertex, $-1$ at the initial vertex, and the algebraic sum when endpoints coincide.
This definition packages the standard incidence pairing of an edge-flow against a vertex as a single integer, ready for finite-support algebra.
proof idea
Pure definition: evaluate the free $1$-chain as a finitely supported function and sum $n\cdot I(e,v)$ over edges $e$ with coefficient $n$, using the already-defined incidence coefficient. No lemmas or tactics; the body is one Finsupp sum.
why it matters
Local finite-support algebra for the support-decreasing graph argument that identifies vertex boundary coefficients with this incidence sum. Downstream lemmas establish additivity, the singleton and zero cases, equality with the explicit support sum, and vanishing of the incidence sum whenever the free boundary vanishes (conditionally on the identification theorem, and unconditionally once that is in place). Those vanishing statements feed the chain-level winding invariant: boundary-zero flows contribute zero at every vertex, so winding descends to homology and pairs with the fundamental loop to give the left inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.