zeroWindingCycles_bound_of_homologyClass_zero
plain-language theorem explainer
If every singular 1-cycle of winding zero is homologous to zero on S¹, then each such cycle is the boundary of an explicit singular 2-chain. Algebraic topologists working the injective half of H₁(S¹;ℤ) ≅ ℤ cite this bridge from homology vanishing to geometric filling. The proof is a one-line application of the standard cycle-equals-boundary lemma once the homology class is known to vanish.
Claim. Assume that every singular $1$-cycle $z$ on $S^1$ with winding number zero satisfies $[z]=0$ in $H_1(S^1;\mathbb{Z})$. Then for every such $z$ there exists a singular $2$-chain $b$ with $\partial b=z$.
background
The module lifts the path-level winding/displacement invariant of the circle to singular simplices on $S^1=\mathrm{TopCat.sphere},1$. Displacement of a singular $1$-simplex is the real number $2\pi$ times winding, obtained by reparameterizing $\Delta^1$ to the unit interval. The key chain-level identity is that the alternating face sum of displacements on any singular $2$-simplex vanishes (winding kills boundaries), by a convex-simplex homotopy and path-displacement additivity.
Two named targets organize the filling problem. The homology-level target asserts: every $1$-cycle of winding zero has vanishing homology class under the projection $\pi$ from cycles to $H_1$. The geometric target asserts: every such cycle equals the image of some singular $2$-chain under the boundary map into cycles. The module notes that the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is already available from the covering-space winding invariant; full generation remains open pending prism/subdivision machinery.
proof idea
Term-mode one-liner. Fix a $1$-cycle $z$ with winding zero. Apply the hypothesis to obtain $\pi(z)=0$ in homology. Feed that equality into cycle_eq_boundary_of_homologyπ_eq_zero, which converts vanishing of the homology class into an explicit witness $b$ in degree $2$ with $\partial b=z$. No further algebraic topology is invoked.
why it matters
This is the hinge that turns a homology-vanishing statement into the concrete singular filling demanded by the zero-winding bound target. Downstream it is the first arrow in the equivalence between the chain-level filling theorem and monicity of the homology-level winding map, and it is the direct step used when monicity of that map is assumed and one must close the filling target.
In the broader Recognition foundation story this supports the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding is already a left inverse to the fundamental class via the once-around generator. The remaining open piece is generation (every $1$-cycle homologous to an integer multiple of the fundamental cycle), which needs simplicial prism/subdivision operators Mathlib does not yet supply. No axioms or local $S^1$ replacements are used here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.