cycleWinding_integral
plain-language theorem explainer
Every singular 1-cycle on the circle, with integer coefficients, has real winding equal to some integer. This is the first concrete geometric subtarget toward the Mathlib identification H₁(S¹;ℤ)≅ℤ. Downstream closure theorems take it as a named hypothesis and discharge it from finite closed-generator or cyclic-edge decompositions. The declaration is pure Prop packaging: no proof, only the quantified integrality statement.
Claim. The assertion that for every singular $1$-cycle $z$ in the integer singular chain complex of $S^1$, the winding number of $z$ equals some integer $n$ when read as a real: $\mathrm{wind}(z)=n\in\mathbb{Z}\subset\mathbb{R}$.
background
The module lifts path-level winding from CircleWinding to singular simplices of $S^1$. Displacement of a singular $1$-simplex is path displacement after reparameterizing $\Delta^1$ to the unit interval; the key identity is that alternating face displacements of any singular $2$-simplex vanish (winding kills boundaries), by convex telescoping inside $\Delta^2$ plus homotopy invariance of path displacement.
cycleWinding evaluates that chain-level winding map on a degree-$1$ cycle: include the cycle into $C_1(S^1;\mathbb{Z})$ and apply the winding chain map, landing in $\mathbb{R}$. The ambient complex is Mathlib's singular chain complex of TopCat.sphere 1 with $\mathbb{Z}$ coefficients, whose $H_1$ is the strict foundation target tied to the circle generator.
Integrality is not automatic from the real-valued map alone: one needs endpoint cancellation in a finite integer chain so the real winding lands on $\mathbb{Z}$.
proof idea
No proof: this is a bare Prop definition. The body is the universal quantifier over degree-$1$ cycles of the integer singular complex of $S^1$, asserting existence of an integer module element whose real image equals cycleWinding z. Downstream lemmas prove the Prop from spanning or kernel-decomposition hypotheses (closed singular one-cycle lists, directed cycles, cyclic edge lists) by reducing to the already-proved integrality of finite closed-generator lists.
why it matters
Named first concrete geometric subtarget in the doc-comment: integer winding on every singular $1$-cycle, expected from endpoint cancellation. Together with the companion zero-winding-bounds subtarget, it feeds circleH1ZIsoInt_of_integral_winding_of_zeroWinding_bounds, the final Mathlib $H_1$ closure ("integer winding on cycles and filling of zero-winding cycles").
Several discharge routes land here: spanning by closed singular generator lists, free-boundary-kernel decomposition into directed cycles or cyclic edge lists, and the unconditional integrality theorem once those geometric inputs are available. With winding-kills-boundaries and the fundamental loop mapping to $1$, integrality supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$; surjectivity still needs generation by the fundamental cycle. The ambient complex is flagged as the chain-level object for the strict T8-linked $H_1$ target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.