circleH1ZIsoInt_holds
plain-language theorem explainer
The first singular homology of the circle with integer coefficients is isomorphic to ℤ, with no remaining hypotheses. Anyone citing the Mathlib-backed H₁(S¹;ℤ) ≅ ℤ certificate in the T8 dimension or linking arguments needs this. The proof is a one-line discharge: feed the unconditional zero-winding filling theorem into the already-proved conditional closure.
Claim. There exists an isomorphism $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$ in the category of $\mathbb{Z}$-modules (Mathlib singular homology), with no extra hypotheses.
background
The module develops the winding invariant on singular 1-simplices of $S^1$. Displacement of a singular 1-simplex is the path displacement of its reparameterization to the unit interval; the key identity is that alternating face sums of displacements vanish on every singular 2-simplex (winding kills boundaries). Together with the fact that the fundamental loop has winding 1, this yields a left inverse to the fundamental class on $H_1$.
The target certificate circleH1ZIsoInt is the proposition that Mathlib's first singular homology of the circle is isomorphic, as a $\mathbb{Z}$-module, to $\mathbb{Z}$. Upstream, the conditional theorem states that this certificate follows once every zero-winding singular 1-cycle is a boundary. That geometric input is now closed: every zero-winding cycle bounds via the free-prism construction, with no axioms or sorry.
proof idea
One-line term proof. Apply the conditional closure circleH1ZIsoInt_of_zeroWinding_bounds, whose only remaining premise is the zero-winding filling theorem, and supply zeroWindingCycles_bound_holds. That premise itself comes from the free-prism generation equivalence for oriented cyclic families. No further case analysis or cohomology computation is performed at this site.
why it matters
This is the unconditional Mathlib $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ certificate required by the strict T8 dimension replacement. Downstream it feeds circle_H1_holds and bridge_of_forces_D3 on the public spine, the detection half detectsNontrivialLinking_three (unknot complement in $S^3$ retracts onto a core circle whose $H_1$ is a retract of $\mathbb{Z}$), and the full forcing certificate complete_forcing_chain_tminus2_to_t8. Verification audits record it as t8_circle_h1_iso_proved. In the Recognition forcing chain this underwrites the linking obstruction that forces $D=3$ (T8), rather than an arithmetic encoding of dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.