circleH1MathlibComputation_of_iso_int
plain-language theorem explainer
Given an isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ as $\mathbb{Z}$-modules, the final Mathlib computation certificate for circle homology is fully filled. Anyone routing the T8 dimension-forcing handoff through pinned Mathlib singular homology cites this. The proof is a three-field structure pack: API availability is already proved in-module, the target identity is definitional (`rfl`), and the iso is the hypothesis.
Claim. If there is a nonempty isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ in $\mathbf{Mod}_{\mathbb{Z}}$, then the Mathlib computation interface is inhabited: the singular-homology functor API is available, the project's circle $H_1$ object equals Mathlib's $H_1(S^1;\mathbb{Z})$, and that object is isomorphic to $\mathbb{Z}$.
background
This module is the Mathlib cohomology bridge contract for the T8 replacement path. Mathlib already exposes the singular homology functor API, but dimension forcing needs a pinned computation of $H_1(S^1;\mathbb{Z})$ (and later an Alexander-duality bridge from circle-complement homology). The module records that backend object without faking it via project-local cohomology encodings.
The strong closure certificate is the proposition that the concrete circle homology object is isomorphic, in $\mathbf{Mod}_{\mathbb{Z}}$, to the integer module. The final import interface is a three-field Prop structure: (i) the singular homology functor exists in the pinned Mathlib, (ii) the project's circle $H_1$ definition equals Mathlib's evaluation of that functor on $S^1$ with $\mathbb{Z}$ coefficients, and (iii) the strong iso certificate holds.
Upstream, the API-availability theorem is already discharged by exhibiting AlgebraicTopology.singularHomologyFunctor. The target-identity field is a definitional equality against that same Mathlib object.
proof idea
Term-mode structure constructor, not a tactic script. Field one is filled by the already-proved API-availability theorem (which returns the Mathlib singular homology functor and a reflexivity witness). Field two is rfl: the project's circle $H_1$ is definitionally the Mathlib evaluation on TopCat.sphere 1. Field three is the hypothesis, the nonempty iso $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. No further algebraic work.
why it matters
This is the one-direction half of the equivalence between the Mathlib computation interface and the strong target $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The sibling biconditional uses it as the reverse constructor. Downstream, the geometric-bridge theorem applies it after deriving the iso from the geometric bridge, producing the certificate consumed by the strict T8 handoff.
In the Recognition forcing chain, T8 forces $D=3$ spatial dimensions. The cohomology-bridge contract is the Mathlib-backed replacement for the concrete $S^1$ cohomology encoding that path currently uses. Filling this interface from a genuine Mathlib computation (rather than a project-local stand-in) is exactly the upgrade the module doc asks for. The geometric bridge is the interim filler; a future Mathlib-native computation of circle homology would discharge the same interface directly through this lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.