mathlibCircleLinkingBackend_of_circleH1MathlibComputation
plain-language theorem explainer
Given a filled Mathlib computation interface for H₁(S¹; ℤ) ≅ ℤ, the Mathlib circle-linking backend object is inhabited. Dimension-forcing and T8 authors cite this to route D = 3 through pinned singular homology rather than a project-local S¹ encoding. The proof is a two-step term composition: nonvanishing from the computation interface, then backend construction from nonvanishing.
Claim. If the Mathlib singular-homology API is available, the project's circle homology object equals Mathlib's $H_1(S^1;\mathbb{Z})$, and that group is isomorphic to $\mathbb{Z}$, then there exists a Mathlib circle-linking backend: a package whose linking support on spatial dimension $D$ is equivalent to $D = 3$ together with nonvanishing of that concrete $H_1(S^1;\mathbb{Z})$.
background
The Mathlib Cohomology Bridge module records the exact backend needed to replace the project's concrete $S^1$ cohomology encoding for T8 (forcing three spatial dimensions). Mathlib already exposes the singular homology functor API; what is still missing for a clean handoff is a pinned computation of reduced circle homology plus an Alexander-duality bridge from circle-complement homology to that group. The module deliberately refuses to fake the backend by reusing a project-local nontriviality lemma.
CircleH1MathlibComputation is the final import interface: singular homology API present, the project's circleH1Z definitionally equal to Mathlib's $H_1(S^1;\mathbb{Z})$, and an isomorphism circleH1Z ≅ ℤ. MathlibCircleLinkingBackend packages API availability, nonvanishing of that homology object, and the linking characterization supportsLinking D ↔ (D = 3 ∧ circleH1ZNonzero). Upstream, nonvanishing is recovered from the iso-to-ℤ field via circleH1ZNonzero_of_mathlib_computation, and the backend is built from nonvanishing via mathlibCircleLinkingBackend_of_circleH1ZNonzero.
proof idea
One-line term composition. From the computation interface C, apply circleH1ZNonzero_of_mathlib_computation (which unpacks C.h1_iso_int and routes through circleH1ZNonzero_of_iso_int) to obtain circleH1ZNonzero. Feed that witness into mathlibCircleLinkingBackend_of_circleH1ZNonzero, which is itself the reverse direction of the iff relating backend inhabitance to circle-H1 nonvanishing. No extra case analysis or cohomology computation is performed here.
why it matters
This is the last glue step from the strong Mathlib computation interface to the backend object that T8's linking characterization is allowed to depend on. Downstream, mathlibBackendHandoffCertificate packages the bridge contract, target certificate, imported-circle identity, and the computation-iff-iso-int equivalence; this theorem supplies the backend inhabitance half of that handoff story.
In the Recognition forcing chain, T8 forces $D = 3$ spatial dimensions. The intended Mathlib path runs linking support through concrete $H_1(S^1;\mathbb{Z})$ nonvanishing rather than a hand-rolled circle model. Filling CircleH1MathlibComputation from Mathlib's actual homology computation (not a local stand-in) would discharge the remaining external target and let dimension forcing cite a fully pinned singular-homology backend.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.