circleH1ZIsoInt_of_mathlib_computation
plain-language theorem explainer
Given a Mathlib-backed computation certificate for the first singular homology of the circle, the strong isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ holds as $\mathbb{Z}$-modules. Cohomology-bridge and dimension-forcing arguments cite this extraction when closing the Mathlib backend contract. The proof is a one-line field projection from the computation interface.
Claim. If a Mathlib computation certificate for the circle is available (singular homology API present, the project's first homology of $S^1$ identified with Mathlib's singular homology of the 1-sphere over $\mathbb{Z}$, and an isomorphism to the integer module), then $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ as objects of $\mathbf{Mod}_{\mathbb{Z}}$.
background
This module is the Mathlib cohomology bridge contract. Mathlib already exposes the singular homology functor API, but the T8 replacement path needs a pinned computation of the (reduced) homology or cohomology of $S^1$, plus an Alexander-duality bridge from circle-complement homology. The module deliberately refuses to fake that backend by recycling a project-local nonvanishing lemma.
The strong closure certificate asserts that the project's circle homology object is isomorphic, in the category of $\mathbb{Z}$-modules, to $\mathbb{Z}$ itself. The computation interface packages three obligations: the singular homology API is available; the project's circle homology equals Mathlib's evaluation of the singular homology functor (degree 1, coefficients $\mathbb{Z}$) on the topological 1-sphere; and the isomorphism certificate itself.
proof idea
One-line term proof. The hypothesis is an inhabitant of the computation interface structure, whose third field is exactly the strong isomorphism certificate. The proof projects that field and stops.
why it matters
This is the forward extraction from the final Mathlib computation interface to the strong certificate $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module exists so that T8 (forcing three spatial dimensions) can eventually rest on a Mathlib-backed circle computation and Alexander duality, rather than a local stand-in. Sibling lemmas convert the same interface into nonvanishing of circle homology. No downstream consumers are wired yet; the open work is to inhabit the computation interface from pinned Mathlib, not from a project-local replacement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.