singularWindingSum_cyclic_integral
plain-language theorem explainer
A cyclically connected finite family of singular 1-simplices on S¹ has total winding equal to an integer. Anyone extracting directed cycles from free edge-chains cites this for the winding_integral field. The proof reduces to the path-level closed-walk integrality lemma via the singular-edge-to-path bridge, then cancels the 2π factor.
Claim. Let $e_0,\ldots,e_{k-1}$ be singular $1$-simplices on $S^1$ such that the terminal $0$-face of $e_i$ equals the initial $0$-face of $e_{i+1\bmod k}$ for every $i$. Then $\sum_{i=0}^{k-1} W(e_i)\in\mathbb{Z}$, where $W$ is the real-valued winding of a singular edge.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$, and proves that winding kills boundaries. A singular $1$-simplex is an element of the singular simplicial set of $\mathrm{TopCat.sphere},1$ in degree $1$. Each such edge has an initial and terminal $0$-face (the two face maps $\delta_1,\delta_0$), and can be reparameterized as a continuous path $I\to S^1$ via the singular-edge-to-path bridge.
Path displacement is the endpoint difference of the canonical real lift of a path on $S^1$; winding is displacement divided by $2\pi$. The upstream path-form result states: if a family of paths is cyclically connected (terminal of $f_i$ equals initial of $f_{i+1\bmod k}$), then the sum of displacements is an integer multiple of $2\pi$. The present theorem is the same statement at the level of singular edges rather than bare paths.
proof idea
First convert the face-matching hypothesis into path endpoint matching: the path of $e_i$ ends where the path of $e_{i+1\bmod k}$ begins, using the endpoint lemmas for the singular-edge path and congruence on vertex points.
Apply the path-level closed-walk integrality theorem to the family of singular-edge paths, obtaining an integer $m$ with total displacement equal to $m\cdot 2\pi$.
Rewrite the sum of singular windings as the sum of path displacements divided by $2\pi$ (termwise via the winding-equals-displacement identity, then factor the constant out of the finite sum). Substitute the displacement identity and cancel $2\pi\neq 0$, leaving the integer $m$.
why it matters
This is the integrality engine for multi-edge cyclic edge-list pieces: once a directed cycle is extracted as a cyclically connected singular-edge family, the total winding is automatically an integer from the combinatorial face-chaining alone, with no prism or subdivision operator.
Downstream, it feeds the packaged homological content of cyclic extraction: a cyclically connected family assembles into a directed-cycle free term whose free edge-chain is a genuine degree-$1$ cycle with integer winding. It is also used when evaluating the winding chain map on a raw free edge-family sum.
In the module's larger program, together with the kills-boundaries identity and the fact that the once-around generator has winding $1$, this supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Surjectivity still needs a simplicial prism/subdivision operator that Mathlib singular homology does not yet provide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.