mathlibCircleLinkingBackend_from_circleH1ZNonzero
plain-language theorem explainer
A proof that Mathlib's first singular homology of the circle is nonvanishing assembles the full Mathlib circle-linking backend required by the T8 replacement. Dimension auditors and T6–T8 spine checks cite this builder. It hard-codes linking support as equality to spatial dimension 3, packages the given nonvanishing hypothesis with the singular-homology API witness, and discharges the linking-equivalence field by a two-direction split.
Claim. From a proof that the Mathlib object $H_1(S^1;\mathbb{Z})$ is not the zero module, one obtains a Mathlib circle-linking backend whose support predicate holds of a spatial dimension $D$ if and only if $D=3$, and whose linking characterization is routed through that same nonvanishing fact together with the singular-homology API.
background
The Mathlib Cohomology Bridge module records the exact backend needed to replace the current concrete $S^1$ cohomology encoding used in dimension forcing. Mathlib already exposes the singular homology functor API; T8's replacement additionally needs a Mathlib-backed nonvanishing of reduced circle homology and a route from that computation into the linking characterization of spatial dimension.
The target structure MathlibCircleLinkingBackend packages four fields: a support predicate on dimensions, a witness that the singular homology API is available, a proof that the concrete Mathlib object $H_1(S^1;\mathbb{Z})$ is nonzero, and an equivalence stating that linking is supported at $D$ precisely when $D=3$ and that nonvanishing holds. The nonvanishing proposition is simply $\neg\mathrm{IsZero}(H_1(S^1;\mathbb{Z}))$ in the module category.
Upstream, the singular-homology API availability is already closed unconditionally, and the framework's T8 circle-H1 nonvanishing replacement is likewise closed. Spatial dimension $D=3$ is the T8/T9 landmark forced by linking.
proof idea
Structure constructor, not a deep argument. The support field is set definitionally to $\mathrm{fun}, D \mapsto D=3$. The API field is filled by the existing theorem that Mathlib supplies singularHomologyFunctor. The circle-H1 field is the input hypothesis. The linking-equivalence field is discharged by introducing $D$ and splitting the biconditional: from $D=3$ one rebuilds the pair $\langle D=3,, h_{H_1}\rangle$; from a pair one projects the first component.
why it matters
This builder is the constructive half of the equivalence that the remaining backend object is nonempty if and only if circle-H1 nonvanishing holds. Downstream, the T6–T8 spine audit uses it to certify that the Mathlib backend still encodes $D=3$ when given only that nonvanishing fact (audit theorem t8_backend_still_encodes_D3), and the bundled July 2026 honesty certificate depends on that encoding check.
In the Recognition forcing chain this sits at T8 (three spatial dimensions forced by linking). The module deliberately refuses to fake the backend by reusing the older Alexander-duality circle-cohomology stub; this definition is the honest packaging step once Mathlib nonvanishing is in hand. It does not itself compute $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$; it only promotes nonvanishing into the full linking-backend contract.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.