zeroWindingCycles_bound_holds
plain-language theorem explainer
Every singular integer 1-cycle on the circle with vanishing winding number is a singular 2-boundary. Homology workers cite this as the filling half of the integer comparison map H₁(S¹;ℤ) → ℤ. The argument is a one-line transfer: free-coordinate prism generation is already proved, and an equivalence identifies that target with zero-winding filling.
Claim. Every singular integer $1$-cycle $z$ on $S^1$ with cycle winding number zero is a boundary: there exists a singular $2$-chain $b$ such that $z$ equals the image of $b$ under the boundary map into $1$-cycles.
background
The module lifts path-level winding on $S^1$ to singular simplices. Displacement of a singular $1$-simplex is the path displacement of its reparameterization to the unit interval; the alternating face sum of any singular $2$-simplex has vanishing displacement (winding kills boundaries). Together with the fact that the fundamental loop has winding one, this yields a left inverse to the fundamental class on $H_1(S^1;\mathbb{Z})$.
Surjectivity of the integer comparison needs the converse filling statement: every zero-winding $1$-cycle bounds. That statement is packaged as the proposition zeroWindingCycles_bound. Upstream, free-coordinate prism generation for oriented cyclic families is already closed by splitting into terminal-side and path-base corrections. An equivalence theorem identifies that free-prism target with zero-winding filling, using raw/free $C_2$ transport so the only geometric content is the filling construction itself.
proof idea
One-line wrapper under classical logic. Apply the forward direction of the equivalence between free-coordinate prism generation and zero-winding filling, feeding in the already-proved free-prism generation theorem (itself obtained by combining the two split correction halves). No new geometric construction appears at this node.
why it matters
This is the missing filling half that upgrades the split-injective winding map to a full isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Downstream, circleH1ZIsoInt_holds quotes it directly: integer-valued winding on cycles was already closed; with zero-winding filling closed too, the Mathlib first-homology computation holds with no remaining hypotheses. The same fact discharges mathlibCircleLinkingBackend_holds, the circle-linking backend required by the strict T8 dimension replacement ($D=3$). In the forcing chain, a clean singular-homology computation of the circle is the topological input that lets the eight-tick octave and spatial dimension step sit on Mathlib rather than a project-local $S^1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.