edgeContribution
plain-language theorem explainer
The contribution of one singular 1-simplex to the boundary coefficient at a vertex is the product of its free-chain coefficient and its incidence number at that vertex. Anyone unpacking explicit boundary sums on free singular 1-chains of S¹ cites this local term. The body is a one-line product of the edge coefficient and the incidence coefficient.
Claim. For a free singular $1$-chain $c$ on $S^1$, a singular $1$-simplex $e$, and a singular $0$-simplex $v$, the edge contribution equals $\mathrm{coeff}_c(e)\cdot I(e,v)$, where $I(e,v)$ is the incidence number of $e$ at $v$ ($+1$ if $v$ is terminal, $-1$ if initial, and their algebraic sum if both endpoints coincide).
background
The module lifts the path-level winding/displacement invariant on the circle to singular simplices of $\mathrm{TopCat.sphere},1$ and proves the chain-level fact that displacement kills boundaries. That identity, with the generator evaluation, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Singular $0$- and $1$-simplices are the actual objects of the singular simplicial set of $S^1$. The free $\mathbb{Z}$-module on singular $1$-simplices carries an explicit coefficient map. The incidence coefficient of a directed singular edge at a vertex is $+1$ at the terminal endpoint, $-1$ at the initial endpoint, and the algebraic sum when the edge is a loop.
Edge contribution is the local summand that appears when a boundary coefficient at a vertex is expanded over the edge support of a free $1$-chain.
proof idea
One-line definition: the free-module coefficient of the edge in the chain, multiplied by the incidence coefficient of that edge at the given vertex. No tactics or lemmas beyond those two component definitions.
why it matters
Four immediate consumers sit in the same module. The boundary incidence sum equals the finite support sum of edge contributions. A supported non-loop edge, read in its sign-selected orientation, contributes positively at its terminal vertex (the local positivity fact used to force a compensating outgoing edge in a balanced flow). In a balanced flow, a positive contribution at a vertex forces some negative contribution at the same vertex (the algebraic core of the next-edge existence step). A negative contribution forces the sign-selected orientation to start at that vertex.
Those lemmas assemble the walk-along-a-cycle argument on free singular $1$-chains of $S^1$. In the Recognition foundation this supports the winding homomorphism as a left inverse to the fundamental class, completing the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation/surjectivity half remains open pending a simplicial prism or subdivision operator not yet in Mathlib.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.