windingChainMap_freeToChain_orientedChain_sum
plain-language theorem explainer
For any finite family of oriented singular edges on S¹, the winding chain map applied to the free-to-singular image of their summed free chains equals the sum of the individual oriented windings. Anyone assembling multi-edge directed cycles from balanced flows cites this linearity step. The proof is a two-line sum-congruence reducing to the single-edge case.
Claim. Let $o : \mathrm{Fin}\, k \to$ (oriented singular $1$-edges on $S^1$). Then $W\bigl(\iota(\sum_i (o_i).\mathrm{chain})\bigr) = \sum_i W^{\mathrm{or}}(o_i)$, where $W$ is the winding chain map $C_1(S^1;\mathbb{Z})\to\mathbb{R}$, $\iota$ embeds the free $1$-chain module into singular chains, and $W^{\mathrm{or}}$ is singular winding with a sign flip on backward edges.
background
The module lifts path-level winding on $S^1$ to singular $1$-simplices and proves that displacement kills boundaries of $2$-simplices, giving a homology invariant. The winding chain map $W:C_1(S^1;\mathbb{Z})\to\mathbb{R}$ sends each free generator indexed by a singular $1$-simplex $s$ to integer multiples of the winding number of $s$.
An oriented singular edge pairs a singular $1$-simplex with a forward/backward orientation. Its free chain is the corresponding generator (or its negative), and its oriented winding is $\pm$ the singular winding accordingly. The free-to-chain map $\iota$ realises free generators as the matching coproduct summands in $C_1(S^1;\mathbb{Z})$.
The single-edge identity already states $W(\iota((o).\mathrm{chain}))=W^{\mathrm{or}}(o)$. The present result is the finite-sum extension needed when a directed cycle is assembled from several oriented edges rather than one closed loop.
proof idea
Term-mode proof by linearity. Rewrite both sides with map_sum (once for $W$, once for $\iota$), then apply Finset.sum_congr and discharge each summand by the single-edge lemma windingChainMap_freeToChain_orientedChain. No new analytic content: pure additivity of the two module morphisms.
why it matters
Feeds directedCycleFreeTerm_of_orientedCyclicFamily, which packages a cyclically connected family of oriented edges into a DirectedCycleFreeTerm (a genuine degree-$1$ cycle with integer winding). That construction generalises the unoriented directedCycleFreeTerm_of_cyclicFamily to the sign-selected orientations produced by balanced-flow walk extraction, and is the homological half of building OrientedCyclicFamilyTerm.
In the broader module story this is a brick in the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding is a left inverse to the fundamental class. The generation/surjectivity half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. No Recognition forcing-chain landmark (T5–T8, RCL, $\varphi$) is touched directly; the result is pure singular-homology infrastructure for circle winding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.