mathlibCircleLinkingBackend_of_circleH1ZIsoInt
plain-language theorem explainer
An isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ as $\mathbb{Z}$-modules yields a nonempty Mathlib circle-linking backend. Dimension-forcing and winding-chain authors cite it to hand off the strict T8 replacement to concrete singular homology. The proof is a one-line composition: iso implies nonvanishing, nonvanishing builds the backend.
Claim. If the first singular homology of the circle with integer coefficients is isomorphic to $\mathbb{Z}$ as a $\mathbb{Z}$-module, then there exists a Mathlib circle-linking backend: a structure whose linking support predicate on dimension is equivalent to "$D=3$ and circle $H_1$ is nonvanishing," routed through Mathlib's singular homology API.
background
The Mathlib Cohomology Bridge module records the backend needed to replace the project's concrete $S^1$ cohomology encoding for the T8 spatial-dimension step. Mathlib already exposes singular homology functors; what is missing is a pinned computation of $H_1(S^1;\mathbb{Z})$ together with a linking bridge that routes through that computation rather than a project-local stand-in.
The strong closure certificate is the proposition that $\mathrm{circleH1Z}$ (Mathlib's first singular homology of the circle over $\mathbb{Z}$) is isomorphic, in the category of $\mathbb{Z}$-modules, to $\mathbb{Z}$ itself. Nonvanishing of that object is the weaker target: it is not the zero object. The backend structure packages API availability, that nonvanishing fact, and the biconditional that linking is supported precisely when the ambient dimension is $3$ and circle $H_1$ is nonzero.
Upstream, computing the homology as $\mathbb{Z}$ immediately closes nonvanishing, because $\mathbb{Z}$ is not the zero module. Separately, nonvanishing alone is already equivalent to existence of a backend object.
proof idea
Term-mode one-line wrapper. From the iso hypothesis, apply circleH1ZNonzero_of_iso_int (if $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, the homology object cannot be zero, else $\mathbb{Z}$ would be zero by transport of isomorphisms). Feed that nonvanishing witness into mathlibCircleLinkingBackend_of_circleH1ZNonzero, which is the right-to-left direction of the equivalence between backend existence and circle-$H_1$ nonvanishing. No extra construction is performed here.
why it matters
This is the preferred strong entry point into the Mathlib-backed linking backend required by the strict T8 replacement (forcing $D=3$ spatial dimensions in the Unified Forcing Chain). Downstream, the geometric bridge builds the backend by first producing the iso certificate and then calling this theorem. The CircleWindingChain module routes several partial discharges the same way: mono of the winding homology map; cyclic edge-list decompositions with zero-winding bounds; extraction steps; large-support extraction; and the residual zero-winding bound after the finite-flow half is unconditional. The in-module handoff certificate also consumes it. Until Mathlib supplies a pinned $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ computation, callers still discharge the iso hypothesis by project-side geometric or combinatorial bridges; this lemma keeps that handoff uniform.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.