mathlibCircleLinkingBackend_nonempty_iff_circleH1ZNonzero
plain-language theorem explainer
Existence of a Mathlib-backed circle-linking backend is equivalent to nonvanishing of the first singular homology of the circle with integer coefficients. Anyone tracking the T8 spatial-dimension forcing replacement cites this biconditional. The proof is a two-direction constructor: project the backend's built-in nonvanishing field, or rebuild the backend from that hypothesis via the dedicated constructor.
Claim. There exists a Mathlib circle-linking backend if and only if the first singular homology module $H_1(S^1;\mathbb{Z})$ is nonzero (not the zero object in the module category).
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 still needs a Mathlib-backed computation of reduced circle cohomology and an Alexander-duality bridge from circle-complement homology to that group.
The backend structure packages four pieces: a linking-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 a linking characterization that forces support exactly when the dimension is $3$ and that nonvanishing holds. The nonvanishing proposition is simply that this homology object is not the zero object in the module category.
Upstream, a dedicated constructor builds a full backend from any proof of circle $H_1$ nonvanishing, setting support to the predicate $D=3$ and routing linking through that fact. The Foundation layer already closes the nonvanishing target unconditionally via the completed forcing chain.
proof idea
Term-mode constructor on the biconditional. Left-to-right: from a nonempty backend, unpack the witness and return its circle_h1_nonzero field. Right-to-left: feed the nonvanishing hypothesis into mathlibCircleLinkingBackend_from_circleH1ZNonzero, which assembles a backend with support predicate $D=3$, the available singular-homology API witness, the given nonvanishing proof, and the linking characterization proved by rewriting. Wrap that backend in Nonempty. No further homology computation occurs here.
why it matters
This is the hinge that collapses the remaining Mathlib backend obligation to a single concrete homology fact. Downstream, the two one-sided projections are immediate: nonempty backend implies nonvanishing, and nonvanishing implies nonempty backend. Both feed the checked cohomology-bridge contract and the Mathlib backend handoff certificate, which package API availability, the circle $H_1$ target certificate, and the current linking characterization.
In the Recognition forcing chain this sits under T8 ($D=3$ spatial dimensions). The backend's linking field is exactly the $D=3$ characterization routed through Mathlib $H_1(S^1;\mathbb{Z})$ rather than the older concrete circle-cohomology encoding. Closing the equivalence means the T8 replacement no longer depends on a richer external package once nonvanishing is in hand; the module deliberately refuses to fake that backend by reusing the prior Alexander-duality nonvanishing lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.