circleH1ZIsoInt_of_directedCycles_of_zeroWinding_bounds
plain-language theorem explainer
Obtains the Mathlib integer isomorphism H₁(S¹;ℤ) ≅ ℤ from two geometric inputs: every balanced free singular 1-chain decomposes into directed cycles, and zero-winding cycles bound (are homologous to zero). Cited by anyone closing the singular-homology comparison for the circle in this foundation stack. Proof is a one-line wrapper: the cycle decomposition yields integer-valued winding on all 1-cycles, which with the zero-winding bound feeds the integral-winding H₁ closure.
Claim. Assume every free singular $1$-chain in the kernel of the free boundary map decomposes as a finite sum of directed cycle pieces, and every singular $1$-cycle of winding zero is a boundary. Then the Mathlib bridge isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ holds.
background
The module lifts path-level winding on $S^1$ to singular simplices. Displacement of a singular $1$-simplex is $2\pi$ times winding after reparameterizing $\Delta^1$ to the unit interval; the key identity is that displacement kills boundaries of singular $2$-simplices (telescoping via convexity of $\Delta^2$ and homotopy invariance of path displacement). Together with the once-around generator mapping to $1$, this gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The remaining generation half needs every $1$-cycle homologous to an integer multiple of the fundamental cycle. The abstract target freeBoundaryKernel_decomposesIntoDirectedCycles states that every free edge-chain with vanishing free boundary is a finite list of directed cycle terms. From that, integer winding on all singular $1$-cycles follows. The companion hypothesis zeroWindingCycles_bound supplies filling of the zero-winding kernel.
Upstream, circleH1ZIsoInt_of_integral_winding_of_zeroWinding_bounds already closes the Mathlib H₁ isomorphism from those two concrete geometric subtargets (integer winding plus zero-winding filling).
proof idea
Pure one-line term wrapper. First apply cycleWinding_integral_of_freeBoundaryKernel_decomposesIntoDirectedCycles to the directed-cycle decomposition hypothesis, obtaining integer-valued winding on every singular $1$-cycle. Pass that integral-winding fact together with the zero-winding bound into circleH1ZIsoInt_of_integral_winding_of_zeroWinding_bounds, which itself reduces to generation of the fundamental-cycle boundary class and thence to the Mathlib bridge isomorphism circleH1ZIsoInt.
why it matters
This is the final packaging step for Mathlib H₁ closure on the circle: it replaces the concrete integral-winding hypothesis by the more structural directed-cycle decomposition of balanced free edge-flows, keeping only the zero-winding filling bound. The module doc frames the goal as the full comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (injective half from winding-kills-boundaries plus generator evaluation; surjective half from cycle generation). Downstream the directed-cycle extraction engine sits in the same chain, supplying the one-step $\ell^1$-decreasing split used to justify the abstract decomposition. In the broader Recognition foundation this pins the singular-homology side of the circle before any physics-facing forcing (T5–T8) is invoked; it does not itself touch $\phi$, the eight-tick octave, or dimension forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.