circleH1ZIsoInt_of_integral_winding_of_zeroWinding_bounds
plain-language theorem explainer
Integer winding of every singular 1-cycle on S¹, together with filling of zero-winding cycles, yields the Mathlib isomorphism H₁(S¹;ℤ) ≅ ℤ. Cite this when closing the generation half of circle homology from those two geometric subtargets. The proof is a two-step term composition: the subtargets imply boundary-generation of the fundamental cycle, which already implies the iso.
Claim. Assume every singular $1$-cycle on $S^1$ has integer winding number, and every zero-winding singular $1$-cycle is a singular $2$-boundary. Then $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ via the Mathlib comparison isomorphism.
background
The module lifts path-level winding on $S^1$ to singular $1$-simplices via simplexDisplacement (displacement $=2\pi\times$ winding after reparameterizing $\Delta^1$ to $[0,1]$). The key chain identity is that displacement kills boundaries: for any singular $2$-simplex the alternating face sum of displacements vanishes, by convexity of $\Delta^2$ and homotopy invariance of path displacement. With the fundamental loop sending to winding $1$, this gives a left inverse $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$.
Surjectivity (every $1$-cycle homologous to an integer multiple of the fundamental cycle) is packaged as boundary-generation. Two concrete geometric props feed it: cycleWinding_integral (every cycle has integer winding, from endpoint cancellation in a finite integer chain) and zeroWindingCycles_bound (every zero-winding cycle is a $2$-boundary, the filling theorem). The target circleH1ZIsoInt is the full Mathlib $\mathbb{Z}$-coefficient isomorphism.
proof idea
Pure term composition, no tactics. First apply fundamentalCycle_boundary_generates_of_integral_winding_of_zeroWinding_bounds to the two hypotheses: for a cycle $z$, take integer $n$ equal to its winding, subtract $n$ times the fundamental cycle, and fill the residual zero-winding cycle, obtaining boundary-generation. Then feed that into circleH1ZIsoInt_of_fundamentalCycle_boundary_generates, itself a thin wrapper through class-generation to the Mathlib iso. No new geometry is proved here.
why it matters
This is the canonical two-hypothesis gate for the Mathlib $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ closure in the CircleWindingChain. Three parents specialize it: circleH1ZIsoInt_of_directedCycles_of_zeroWinding_bounds and circleH1ZIsoInt_of_cyclicEdgeLists_of_zeroWinding_bounds discharge integer winding via free-boundary-kernel decompositions into directed cycles or cyclic edge lists; circleH1ZIsoInt_of_zeroWinding_bounds uses the unconditional integral-winding theorem and leaves only zero-winding filling. In the module narrative this is the generation half that, with the already-proved kills-boundaries identity and fundamental-loop winding $1$, completes the split-injective-plus-surjective comparison. It sits in Foundation homology scaffolding rather than the T0–T8 forcing chain, but supplies the circle $H_1$ fact used wherever RS needs the integer winding generator on $S^1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.