orientedWindingSum_cyclic_integral
plain-language theorem explainer
A cyclically connected family of oriented singular edges on S¹ has integer total oriented winding. Anyone assembling free 1-chains from oriented walks (balanced-flow extraction, cycle decomposition) cites this to know the winding of the resulting cycle is integral. The proof reduces to the path-level closed-walk integrality lemma by reinterpreting each oriented edge as a path and dividing the total displacement by 2π.
Claim. Let $k \in \mathbb{N}$ and let $o : \mathrm{Fin}\,k \to$ (oriented singular edges on $S^1$) satisfy the cyclic gluing condition that the oriented terminal vertex of $o_i$ equals the oriented initial vertex of $o_{i+1 \bmod k}$ for every $i$. Then there exists $n \in \mathbb{Z}$ such that $\sum_i W(o_i) = n$ in $\mathbb{R}$, where $W$ is the oriented winding of an edge occurrence.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular 1-simplices of $S^1$, and proves that displacement kills boundaries of 2-simplices. That identity, together with the fact that the once-around loop has winding 1, supplies the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
An oriented singular edge pairs a singular 1-simplex with a forward/backward orientation; its initial and terminal vertices flip under reversal. The associated path orientedEdgePath is the singular edge path or its reverse. Path displacement is the endpoint difference of the canonical real lift of a path on $S^1$; oriented winding is that displacement divided by $2\pi$.
Upstream, displacementSum_cyclic_intMul already states the path form: a cyclically connected family of continuous paths $f_i : I \to S^1$ has total displacement an integer multiple of $2\pi$. The present theorem is the oriented-edge packaging of that fact.
proof idea
First convert the vertex gluing hypothesis into path endpoint matching: orientedEdgePath_one and orientedEdgePath_zero identify path endpoints with vertexPoint of the oriented terminal/initial vertices, so cyclic vertex equality becomes $(f_i)(1) = (f_{i+1})(0)$.
Apply displacementSum_cyclic_intMul to the family of oriented edge paths to obtain an integer $m$ with $\sum_i \mathrm{pathDisplacement}(f_i) = m \cdot 2\pi$.
Rewrite the winding sum via orientedWinding_eq_pathDisplacement and Finset.sum_div, substitute the displacement identity, and cancel the nonzero factor $2\pi$ (positivity) to conclude the sum of windings equals $m$.
why it matters
Integer total winding is the numerical content needed when an oriented cyclic family is packaged as a genuine degree-1 cycle. Downstream, directedCycleFreeTerm_of_orientedCyclicFamily builds a DirectedCycleFreeTerm from such a family: the signed free edge-chain has vanishing free boundary (oriented telescoping) and carries this integer winding. That generalises the unoriented cyclic extraction to the sign-selected orientations produced by balanced-flow walk extraction.
In the module's larger program, this sits on the path from path displacement through singular simplices toward a winding homomorphism on 1-cycles that is a left inverse to the fundamental class. The generation half (every 1-cycle homologous to an integer multiple of the fundamental cycle) still needs a simplicial prism/subdivision operator that Mathlib singular homology does not yet supply. No Recognition forcing-chain step (T0–T8) is directly invoked here; the result is pure circle homology scaffolding for later RS use of $H_1(S^1)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.