zeroWindingCycles_bound
plain-language theorem explainer
Every singular 1-cycle on S¹ with vanishing winding is a singular 2-boundary. This Prop packages the classical filling half of H₁(S¹;ℤ) ≅ ℤ and is the remaining geometric input once integer winding on cycles is known. Downstream H₁-isomorphism theorems take it as a named hypothesis. The declaration is a bare universal statement, not a proved theorem.
Claim. The proposition that every singular $1$-cycle $z$ in the integer singular chain complex of $S^1$ with winding number zero is a boundary: there exists a singular $2$-chain $b$ such that $z$ is the image of $b$ under the degree-$(2\to 1)$ cycle map.
background
The module lifts path-level winding on $S^1$ to singular simplices. Displacement of a singular $1$-simplex is the real number obtained by reparameterizing $\Delta^1$ to the unit interval and taking path displacement ($2\pi$ times winding). The key identity already proved is that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes, by telescoping inside the convex standard $2$-simplex and homotopy invariance of path displacement.
Winding of a degree-$1$ cycle is the composite of the cycle inclusion into $C_1(S^1;\mathbb{Z})$ with the winding chain map; it lands in $\mathbb{R}$. The ambient complex is Mathlib's singular chain complex of $\mathrm{TopCat.sphere},1$ with integer coefficients, whose $H_1$ is the strict computational target of this foundation layer.
Together with the fact that the fundamental loop has winding $1$, winding supplies a left inverse to the fundamental class (injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). Surjectivity needs every $1$-cycle homologous to an integer multiple of the fundamental cycle, which splits into integer-valued winding plus filling of the zero-winding residual.
proof idea
No proof: the declaration is a def of a Prop. Its body is the raw universal statement that every degree-$1$ cycle $z$ with cycleWinding z = 0 lies in the image of the boundary map from degree $2$ (via toCycles 2 1). The intended discharge path, per the doc-comment, is subdivision or prism operators on singular chains (or an equivalent constructive filling), which Mathlib's singular homology does not yet expose as a ready lemma.
why it matters
This is the second concrete geometric subtarget for closing Mathlib $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Parent theorems such as circleH1ZIsoInt_of_zeroWinding_bounds, circleH1ZIsoInt_of_integral_winding_of_zeroWinding_bounds, and the cyclic-edge-list / directed-cycle / extraction-step variants all take this Prop as a hypothesis and return the full integer comparison isomorphism.
Once integer winding on cycles is unconditional, the doc for the zero-winding-only closure states that this filling theorem is the sole remaining geometric input. That isomorphism is the homology-level half of the circle computation feeding the foundation forcing chain (the singular complex is flagged as the strict T8-adjacent computational target). The module already closed the kills-boundaries identity and the split-injective half; this Prop names the missing generation half.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.