zeroWindingCycles_bound_of_windingHomologyMap_mono
plain-language theorem explainer
If the homology-level winding map H₁(S¹;ℤ) → ℝ is monic, every singular 1-cycle of winding zero is the boundary of a singular 2-chain. Anyone closing the generation half of H₁(S¹;ℤ) ≅ ℤ via winding cites this bridge. The proof is a two-step term composition: monicity forces zero-winding cycles into the zero homology class, then that class condition yields an explicit filling.
Claim. Assume the winding homomorphism $H_1(S^1;\mathbb{Z})\to\mathbb{R}$ is monic. Then every singular $1$-cycle $z$ on $S^1$ with winding number zero is a singular $2$-boundary: there exists a $2$-chain $b$ with $\partial b=z$.
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 key identity is that alternating face displacements of every singular $2$-simplex vanish (winding kills boundaries). That identity lets winding factor through $H_1(S^1;\mathbb{Z})$ as a map into $\mathbb{R}$.
The target proposition zeroWindingCycles_bound is the geometric filling statement: every integer $1$-cycle of winding zero is homologous to zero via an explicit singular $2$-chain. Upstream, monicity of the homology winding map already implies that zero winding forces the homology class itself to vanish. Separately, vanishing of the homology class of a cycle always produces a bounding $2$-chain by the definition of singular homology.
Together with the once-around generator mapping to winding $1$, this is the remaining half needed for the split comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
proof idea
Pure term composition of two prior lemmas. First apply the monicity implication: if the homology winding map is monic, every zero-winding cycle has zero homology class. Feed that hypothesis into the filling lemma: whenever zero winding kills the homology class, every such cycle equals the image of some singular $2$-chain under the boundary-to-cycles map. No new geometric work occurs here.
why it matters
This is the monicity route into the zero-winding filling target that the circle homology computation needs. Downstream, circleH1ZIsoInt_of_windingHomologyMap_mono uses it to conclude $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ once monicity is known, bypassing older cyclic-edge-list interfaces. A sibling theorem obtains the same bound from surjectivity of the fundamental-class map by first deriving monicity, then calling this result.
In the Recognition chain the circle's first homology being $\mathbb{Z}$ underwrites the eight-tick octave (T7) and the discrete winding bookkeeping that feeds later forcing steps. The module doc still flags that full generation via prism/subdivision is not yet supplied by Mathlib singular homology; monicity (or fundamental-class surjectivity) is the abstract substitute that closes the filling half without that machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.