circleH1ZIsoInt
plain-language theorem explainer
The proposition that first singular homology of the circle with integer coefficients is isomorphic to ℤ as a ℤ-module. Dimension-forcing and circle-winding arguments cite it as the Mathlib-backed closure certificate for that classical computation. It is pure definitional packaging: nonemptiness of the module isomorphism, with no proof obligations here.
Claim. There exists an isomorphism of $\mathbb{Z}$-modules $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, where $H_1(S^1;\mathbb{Z})$ denotes the first singular homology of the topological circle (Mathlib's singular homology functor at degree $1$ on $S^1$ with integer coefficients).
background
The Mathlib Cohomology Bridge module records backend objects needed to replace project-local $S^1$ cohomology encodings with Mathlib-native computations. Mathlib already exposes the singular homology functor API, but the T8 dimension-forcing path needs a genuine computation of circle homology (and, nearby, reduced cohomology plus Alexander duality), not a local stand-in.
Upstream, the concrete object is first singular homology of TopCat.sphere 1 with coefficients in the integer module: the value of Mathlib's singular homology functor at degree 1. The classical fact is $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. This declaration turns that fact into a named Prop: nonemptiness of an isomorphism in ModuleCat ℤ between that homology object and $\mathbb{Z}$ itself.
The module contract deliberately refuses to fake the backend by reusing project-local nontriviality lemmas. A future upgrade is expected to discharge the proposition from Mathlib's actual $H_1(S^1;\mathbb{Z})$ computation.
proof idea
Definitional packaging only. The body is the proposition that there is a nonempty isomorphism, in the category of $\mathbb{Z}$-modules, between Mathlib's first singular homology of the circle and the free rank-one integer module. No tactics or lemmas run here. Discharge is deferred to downstream bridges: geometric models, chain homotopy equivalences to the ordinary cellular circle complex, degree-1 quasi-isomorphisms, or the unconditional forcing-chain export.
why it matters
This is the strong final Mathlib closure certificate named in the doc-comment: compute the circle's first singular homology as the integer module. Downstream, Foundation.circle_h1_iso_int asserts the proposition unconditionally via the complete forcing chain from T−1 through T8. CircleH1Computation supplies a family of conditional closures (geometric bridge, homotopy equivalence to the ordinary cellular model, quasi-iso at degree 1) all aimed at this exact proposition shape, so the bridge file stays fixed until the chain-level fact is unconditional. CircleWindingChain also consumes the certificate.
In the Recognition Science forcing chain, T8 forces $D=3$ spatial dimensions. Making $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ a Mathlib-shaped proposition is part of rendering that topological backbone native rather than project-local. The remaining open path is filling the proposition from Mathlib's genuine computation, not a local replacement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.