circleH1ZIsoInt_of_zeroWinding_bounds
plain-language theorem explainer
Assuming every zero-winding singular 1-cycle on S¹ is a 2-boundary, the first singular homology is isomorphic to ℤ as a ℤ-module. Citation target for anyone closing the Mathlib H₁(S¹;ℤ) certificate after the finite-flow half is already unconditional. Proof is a two-argument term applying the joint integral-winding-plus-filling lemma to the unconditional integrality theorem and the remaining filling hypothesis.
Claim. If every singular $1$-cycle $z$ on $S^1$ with winding number zero is the boundary of some singular $2$-chain, then there exists an isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ in the category of $\mathbb{Z}$-modules.
background
The module lifts path-level winding on the circle to singular $1$-simplices of $\mathrm{TopCat.sphere},1$. Displacement of a singular $1$-simplex is $2\pi$ times winding after reparameterizing $\Delta^1$ to the unit interval; the key chain-level identity is that alternating face displacements of every singular $2$-simplex vanish (winding kills boundaries), by convexity of $\Delta^2$ and homotopy invariance of path displacement.
Together with the fact that the once-around generator has winding $1$, this yields a left inverse to the fundamental class on $H_1$, i.e. the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Surjectivity (generation) needs a filling statement for zero-winding cycles.
The target certificate circleH1ZIsoInt is the proposition that $H_1(S^1;\mathbb{Z})$ is isomorphic to $\mathbb{Z}$ as a $\mathbb{Z}$-module. The hypothesis zeroWindingCycles_bound asserts: every $1$-cycle with vanishing cycle winding is the image of some $2$-chain under the boundary-to-cycles map. Integer-valued winding on all $1$-cycles is already available unconditionally via directed-cycle decomposition of the free boundary kernel.
proof idea
One-line term wrapper. Apply circleH1ZIsoInt_of_integral_winding_of_zeroWinding_bounds, which closes the Mathlib $H_1$ certificate from the two geometric subtargets (integral winding on cycles, and filling of zero-winding cycles). Supply the first subtarget by cycleWinding_integral_unconditional (directed-cycle decomposition with classical decidable equality on singular simplices) and the second by the given hypothesis hzero. No further tactic work.
why it matters
This is the last conditional gate before the unconditional Mathlib first-homology computation. Downstream, circleH1ZIsoInt_holds discharges the remaining hypothesis via zeroWindingCycles_bound_holds and obtains $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ with no axioms or sorry. Parallel consumers rebuild nonzero $H_1$, the Mathlib circle-linking backend, and a mono-of-winding-map route to the same iso.
In the Recognition forcing chain the circle-linking backend is required infrastructure for the strict T8 dimension replacement ($D=3$). The doc-comment frames the result as final Mathlib $H_1$ closure after the finite-flow half is already unconditional: only the zero-winding filling theorem remains as geometric input at this node. The module itself uses no project-local $S^1$ replacements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.