circleH1MathlibComputation_iff_iso_int
plain-language theorem explainer
Existence of a Mathlib-backed computation witness for the circle's first singular homology is equivalent to the strong target $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Anyone wiring the cohomology bridge contract or the Mathlib handoff certificate cites this biconditional. The proof is a two-line constructor: project the structure field one way, and rebuild the structure from the iso the other way.
Claim. There exists a Mathlib computation interface witness for the first singular homology of the circle if and only if $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ as objects of $\mathrm{ModuleCat}\,\mathbb{Z}$.
background
This module records the exact Mathlib backend object needed to replace the project's concrete $S^1$ cohomology encoding for the T8 dimension-forcing chain. Mathlib already exposes the singular homology functor API; what is still missing is a pinned computation of $H_1(S^1;\mathbb{Z})$ together with the Alexander-duality bridge from circle-complement homology.
The strong target certificate circleH1ZIsoInt is the proposition that the project's circle-$H_1$ object is isomorphic, in $\mathrm{ModuleCat},\mathbb{Z}$, to the integer module. The structure CircleH1MathlibComputation packages three obligations: the singular-homology API is import-available, the project's circle-$H_1$ equals Mathlib's singular homology of TopCat.sphere 1 with $\mathbb{Z}$ coefficients, and the strong iso holds.
Upstream, circleH1MathlibComputation_of_iso_int already shows that any proof of the strong iso fills the full structure, because the API availability and target-identity fields are discharged by import checks and rfl in this module.
proof idea
Term-mode constructor on the biconditional. Left-to-right: given a nonempty witness ⟨C⟩, return the structure field C.h1_iso_int. Right-to-left: given hiso : circleH1ZIsoInt, wrap it with the upstream constructor circleH1MathlibComputation_of_iso_int hiso and pack the result as ⟨...⟩. No extra algebraic work; the equivalence is purely the projection/injection of the iso field against an already-proved filler.
why it matters
This biconditional is the hinge that lets the bridge treat "Mathlib has computed $H_1(S^1;\mathbb{Z})$" and "the strong iso holds" as interchangeable. Downstream, circleH1TargetCertificate installs it as the field computation_iff_iso_int, and mathlibBackendHandoffCertificate reuses the same field inside the checked handoff for the external Mathlib target.
In the Recognition forcing chain, T8 needs a Mathlib-backed nontriviality of circle cohomology (via Alexander duality) to force $D=3$. The module deliberately refuses to fake that backend with the project-local AlexanderDuality.CircleReducedCohomologyNontrivial; this iff keeps the contract honest until a real Mathlib computation lands. Closing the remaining open obligation is exactly supplying circleH1ZIsoInt from Mathlib rather than from a local stand-in.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.