zeroWindingCycles_bound_of_fundamentalCycleClass_generates
plain-language theorem explainer
If every singular 1-cycle on the circle is homologous to an integer multiple of the fundamental cycle, then every zero-winding 1-cycle bounds a 2-chain. Cited by anyone reducing the filling half of H₁(S¹;ℤ) ≅ ℤ to cycle-class generation. Proof is a one-line composition: generation implies surjectivity of the fundamental homology class, which already yields the zero-winding bound.
Claim. Assume every singular $1$-cycle $z$ on $S^1$ satisfies $[z] = n[\gamma]$ in $H_1(S^1;\mathbb{Z})$ for some $n\in\mathbb{Z}$, where $\gamma$ is the fundamental cycle. Then every singular $1$-cycle with winding number zero is the image of a singular $2$-chain under the boundary map.
background
The module lifts path-level winding on $S^1$ to singular $1$-simplices via simplex displacement (reparameterize $\Delta^1$ to $[0,1]$ and take path displacement). The key identity is that displacement kills boundaries of $2$-simplices: the alternating face sum vanishes by convexity of $\Delta^2$ and homotopy invariance of path displacement. Together with the fact that the fundamental loop has winding $1$, this yields a winding homomorphism on $1$-cycles that is a left inverse to the fundamental class.
What remains for $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is the generation half: every $1$-cycle is homologous to an integer multiple of the fundamental cycle. The hypothesis here is that cycle-class form of generation: for every cycle representative $z$, the homology class of $z$ equals $n$ times the fundamental homology class for some $n$. The target is the zero-winding filling statement: if $\mathrm{cycleWinding}(z)=0$ then $z$ is a $2$-boundary.
Upstream, cycle-class generation already implies surjectivity of the fundamental homology class map (because $\mathrm{homology}\pi$ is epi), and that surjectivity already implies the zero-winding bound via injectivity of the homology-level winding map.
proof idea
One-line term proof. Apply the upstream lemma that cycle-class generation implies surjectivity of the fundamental homology class map, then feed that surjectivity into the already-proved implication from surjectivity to the zero-winding filling target. No new geometric argument appears at this layer.
why it matters
Closes one reduction step in the circle homology comparison that underpins the winding invariant as a complete $H_1$ invariant. The module aims at the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ from winding-kills-boundaries plus winding of the generator equal to $1$; the converse generation half is the remaining geometric work.
This theorem shows that the homology-level generation hypothesis is already enough for zero-winding filling. A nearby comment isolates the still-open geometric obligation: it suffices to prove the fully concrete chain-level statement that every $1$-cycle equals a $2$-boundary plus an integer multiple of the lifted fundamental cycle (subdivision or prism filling of the zero-winding remainder). No downstream consumers are wired yet; the declaration is a pure reduction link in the forcing chain toward that geometric target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.