zeroWindingCycles_homologyClass_zero
plain-language theorem explainer
Names the homology-level zero-winding property: every integer singular 1-cycle on the circle with vanishing winding represents the zero class in first homology. Anyone proving injectivity of the winding map on H₁(S¹;ℤ), or converting zero winding into an explicit 2-chain filling, cites this Prop as the intermediate target. It is a pure definition packaging a universal quantification over cycles; there is no proof body.
Claim. The property asserting that for every singular $1$-cycle $z$ on $S^1$ with integer coefficients, if the winding number of $z$ vanishes, then the homology projection sends $z$ to the zero class in $H_1(S^1;\mathbb{Z})$.
background
The ambient object is the Mathlib singular chain complex of the topological circle $S^1=\mathrm{TopCat.sphere},1$ with coefficients in $\mathbb{Z}$. Degree-1 cycles are the kernel of the boundary $C_1\to C_0$; the homology projection $\pi_1$ quotients those cycles by boundaries to produce $H_1(S^1;\mathbb{Z})$.
Winding is lifted from path displacement on the circle to singular 1-simplices, then extended linearly to chains and restricted to cycles. The resulting real-valued invariant on a cycle $z$ is the composition of the cycle inclusion with the winding chain map. Module documentation records that this invariant kills boundaries (the alternating face sum of displacement on any singular 2-simplex vanishes by a convex-simplex homotopy), so it descends to homology and is a left inverse to the fundamental class: the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The present definition packages the converse direction at the level of classes: zero winding should force the class itself to vanish. By the standard fact that $\pi_1(z)=0$ iff $z$ is a boundary, that class-level statement is exactly what is needed to produce explicit singular 2-chain fillings of zero-winding cycles.
proof idea
No proof: the declaration is a def of a Prop. Its body is the quantified implication "for all degree-1 cycles $z$, cycle winding zero implies homology projection of $z$ is zero." Downstream theorems treat this Prop as a named hypothesis or conclusion in an equivalence web; they do not unfold a constructive argument inside the definition itself.
why it matters
This Prop is the homology-class form of the zero-winding filling target in the circle winding chain module. Four sibling theorems establish its equivalence with two other formulations: (i) monicity of the descended winding map on $H_1$, and (ii) the explicit statement that every zero-winding cycle bounds a singular 2-chain. One direction applies the general lemma that vanishing under $\pi_1$ yields an explicit boundary; the converse uses that boundaries die under $\pi_1$, or that injectivity of the homology winding map forces zero winding to imply zero class.
In the Recognition Science foundation stack this sits on the path to the strict integer computation of $H_1(S^1;\mathbb{Z})$, the topological half of the T8 forcing of three spatial dimensions via the eight-tick / circle generator story. The module already has the kills-boundaries identity and the left-inverse property against the fundamental loop; the missing generation half (every cycle homologous to an integer multiple of the fundamental cycle) still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. Naming the class-level zero-winding target cleanly separates that open generation question from the injectivity/filling equivalences already formalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.