circleH1ZNonzero_of_mathlib_computation
plain-language theorem explainer
Any Mathlib-backed computation of the first singular homology of the circle yields nonvanishing of that group. Dimension-forcing and cohomology-bridge authors cite it to turn the strong iso target H₁(S¹; ℤ) ≅ ℤ into the weaker nonzero predicate the T8 replacement needs. The proof is a one-line application of the iso-implies-nonzero lemma to the structure's iso field.
Claim. If a Mathlib computation package for $H_1(S^1;\mathbb{Z})$ is available (singular-homology API present, the project target equals Mathlib's $H_1(S^1;\mathbb{Z})$, and that group is isomorphic to $\mathbb{Z}$ as a $\mathbb{Z}$-module), then $H_1(S^1;\mathbb{Z})$ is not the zero object in $\mathbf{Mod}_{\mathbb{Z}}$.
background
The Mathlib Cohomology Bridge module records the exact backend 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 link from circle-complement homology.
The project target circleH1Z is the first singular homology of the circle with integer coefficients, viewed as an object of $\mathbf{Mod}_{\mathbb{Z}}$. Nonvanishing means that object is not zero in the categorical sense. The strong closure target is an isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
CircleH1MathlibComputation packages three facts: the singular-homology API is available, the project target equals Mathlib's evaluation of the singular homology functor on $S^1$, and the iso-to-$\mathbb{Z}$ certificate holds. Upstream, circleH1ZNonzero_of_iso_int already shows that any such iso forces nonvanishing, because $\mathbb{Z}$ is not the zero module.
proof idea
One-line term wrapper. Unpack the Mathlib computation structure and feed its h1_iso_int field to circleH1ZNonzero_of_iso_int. That upstream lemma proceeds by contradiction: an iso to $\mathbb{Z}$ plus a zero hypothesis would make $\mathrm{ModuleCat.of},\mathbb{Z},\mathbb{Z}$ zero via transport of isomorphisms, which is false. No new algebraic work occurs here.
why it matters
Closes the nonvanishing half of the final circle-$H_1$ import interface. Downstream, circleH1TargetCertificate records this implication as computation_implies_nonzero, pinning every remaining handoff to the single strong target $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The same arrow feeds mathlibCircleLinkingBackend_of_circleH1MathlibComputation, which builds the Mathlib circle-linking backend from nonvanishing, and the aggregate mathlibBackendHandoffCertificate.
In the Recognition forcing chain this is infrastructure for T8 ($D=3$ spatial dimensions): the bridge must eventually replace the concrete $S^1$ cohomology encoding by a Mathlib-backed computation plus Alexander duality. The declaration does not itself compute the homology; it proves that once Mathlib supplies the iso, nonvanishing (and therefore the linking backend) follows automatically.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.