mathlibCircleLinkingBackend_of_circleH1ZNonzero
plain-language theorem explainer
Given nonvanishing of Mathlib's first singular homology of the circle with integer coefficients, a Mathlib circle-linking backend object exists. Dimension-forcing and cohomology-bridge authors cite it to discharge the backend from the single H₁ computation. The proof is a one-line application of the reverse direction of the nonempty-iff-nonvanishing equivalence.
Claim. If the Mathlib object $H_1(S^1;\mathbb{Z})$ is not the zero object in the category of $\mathbb{Z}$-modules, then there exists a Mathlib circle-linking backend: a structure that routes the $D=3$ linking characterization through that nonvanishing homology computation and the singular-homology API.
background
The module records the exact backend needed to replace the project's concrete $S^1$ cohomology encoding with a Mathlib-backed computation. Mathlib already exposes the singular homology functor API; T8 still needs a genuine computation of circle homology (and later an Alexander-duality bridge from circle-complement homology). The module deliberately refuses to fake that backend by reusing the older concrete nonvanishing lemma.
Here circleH1ZNonzero is the proposition that the concrete Mathlib homology object circleH1Z is not a zero object. The structure MathlibCircleLinkingBackend packages four fields: a dimension-support predicate, a witness that the singular-homology API is available, the circle-$H_1$ nonvanishing fact, and the linking law that supportsLinking D holds if and only if $D=3$ and that nonvanishing holds.
Upstream, mathlibCircleLinkingBackend_nonempty_iff_circleH1ZNonzero states that existence of such a backend is equivalent to the single nonvanishing proposition. The reverse direction of that equivalence is exactly what this theorem applies.
proof idea
One-line term proof. Apply the reverse implication of mathlibCircleLinkingBackend_nonempty_iff_circleH1ZNonzero (the .mpr direction) to the given hypothesis hH1 : circleH1ZNonzero. That iff already constructs the backend structure from nonvanishing on the right-to-left side, so no further field packing is needed here.
why it matters
This is the thin constructor that turns the concrete Mathlib $H_1(S^1;\mathbb{Z})$ nonvanishing fact into the backend object the cohomology-bridge contract demands. Downstream, mathlibCircleLinkingBackend_of_circleH1ZIsoInt and mathlibCircleLinkingBackend_of_circleH1MathlibComputation both reduce to it after deriving nonvanishing from the stronger iso-to-$\mathbb{Z}$ or full computation interfaces. mathlibCohomologyBridgeContract and mathlibBackendHandoffCertificate sit on the same bridge stack.
In the CircleWindingChain module, mathlibCircleLinkingBackend_unconditional cites this theorem with an unconditional nonvanishing witness, so the backend exists without extra hypotheses once that computation is closed. Framework-wise this is infrastructure for the T8 $D=3$ forcing step: linking support is characterized as dimension three precisely when the circle homology is nontrivial, matching the eight-tick / three-spatial-dimension landmark rather than a hand-rolled cohomology encoding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.