edgeCoeff_add
plain-language theorem explainer
Edge coefficients on free singular 1-chains of S¹ are additive in the chain: the coefficient of e in c+d equals the sum of the coefficients in c and in d. Anyone building integer linear combinations of singular edges (edge-list chains, cyclic terms, winding pairings) cites this. The proof is a one-line reduction to Finsupp pointwise addition after unfolding the coefficient map.
Claim. For free singular $1$-chains $c,d$ on $S^1$ and any singular $1$-simplex $e$, the edge coefficient satisfies $\mathrm{coeff}(c+d,e)=\mathrm{coeff}(c,e)+\mathrm{coeff}(d,e)$ in $\mathbb{Z}$.
background
The module works at the singular-chain level on the actual sphere $S^1=\mathrm{TopCat.sphere},1$. A singular $1$-simplex is an element of the singular simplicial set in degree $1$. The free module on those simplices is the explicit $C_1$ object used here: integer finitely supported functions on singular edges.
The edge coefficient of a free chain $c$ at a simplex $e$ is simply the value of that finitely supported function at $e$. The module's larger goal is to lift path displacement/winding from CircleWinding to singular simplices and prove that displacement kills boundaries of $2$-simplices, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Additivity of coefficients is the elementary module structure fact needed before any positivity or pairing argument on edge-list chains.
proof idea
Unfold the coefficient definition: both sides become evaluation of the underlying finitely supported functions. The claim is then exactly pointwise addition of Finsupp values at $e$, discharged by Finsupp.add_apply. No topology or winding enters.
why it matters
Feeds directly into nonnegativity of coefficients along a forward singular edge-list chain (edgeCoeff_singularEdgeListChain_nonneg), which is the bookkeeping step before scaling by the global integer of a cyclic edge-list term. In the CircleWindingChain program this is plumbing for the free $C_1$ module that carries the winding homomorphism: once coefficients behave linearly, edge-list constructions and the kills-boundaries identity can talk about integer combinations without ad-hoc case splits. It does not itself touch T0–T8 or the Recognition Composition Law; it is foundation homology infrastructure for the $H_1(S^1)\cong\mathbb{Z}$ comparison the module advertises.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.