mathlibCohomologyBridgeContract
plain-language theorem explainer
Packages a checked contract for the Mathlib cohomology bridge used by T8: singular-homology API present, circle H1 target certified, the internal circle-H1 object identified with Mathlib singular homology of S^1, nontrivial linking characterized as D=3, and backend nonemptiness tied to circle-H1 nonvanishing. Auditors of the T8 Mathlib replacement and the backend handoff cite it. Proof is a structure assembly: existing certificates plus the DimensionForcing linking iff.
Claim. A checked bridge contract holds: Mathlib's singular homology API is available; the circle $H_1$ target certificate is in force; the internal object $\mathrm{circleH1Z}$ equals Mathlib singular homology $H_1(S^1;\mathbb{Z})$; for every spatial dimension $D$, nontrivial linking is supported if and only if $D=3$; and a nonempty Mathlib circle-linking backend is equivalent to (and constructible from) nonvanishing of that circle $H_1$ group.
background
The module records what is still needed to replace the concrete $S^1$ cohomology encoding in the T8 chain by a pure Mathlib backend. Mathlib already exposes the singular homology functor API; the missing pieces are a Mathlib-backed computation of (reduced) circle homology/cohomology and the Alexander-duality bridge from circle-complement homology to that group. The contract deliberately refuses to fake the backend by reusing the older concrete nonvanishing encoding.
MathlibCohomologyBridgeContract is a Prop-structure bundling seven obligations: API availability; a circle-$H_1$ target certificate; an equality identifying the internal circleH1Z with Mathlib's singularHomologyFunctor applied to TopCat.sphere 1 with $\mathbb{Z}$ coefficients; the linking characterization $\forall D,,\mathrm{SupportsNontrivialLinking}(D)\leftrightarrow D=3$; and three backend clauses relating Nonempty MathlibCircleLinkingBackend to circle-$H_1$ nonvanishing.
Upstream, DimensionForcing supplies the T8 primary pair: linking requires $D=3$ (Alexander duality, no 8-tick or gap-45), and $D=3$ supports nontrivial linking via the Hopf-link witness in $\widetilde{H}_1(S^3\setminus S^1)\cong\mathbb{Z}$. The Foundation layer already closes unconditional circle-$H_1$ nonvanishing and the stronger $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ target.
proof idea
Structure-instance proof. API availability and the circle-$H_1$ target certificate are plugged in by name. Object identity is the existing equality that circleH1Z is Mathlib singular homology of the 1-sphere.
The linking characterization is proved by intro on $D$ and constructor on the biconditional: left-to-right is DimensionForcing.linking_requires_D3; right-to-left rewrites $D=3$ and applies DimensionForcing.D3_has_linking.
Backend implication is a one-step destruct of a nonempty backend witness, projecting its circle_h1_nonzero field. The remaining two fields are the named iff and constructor lemmas relating backend nonemptiness to circleH1ZNonzero.
why it matters
This is the checked contract that the paper-facing handoff certificate consumes: mathlibBackendHandoffCertificate sets bridge_contract := mathlibCohomologyBridgeContract and packages the imported object, the strong $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ interface, the weaker nonvanishing target, and the backend object used by T8.
In the Recognition forcing chain, T8 forces $D=3$ spatial dimensions from nontrivial linking via Alexander duality. The contract freezes the exact Mathlib surface that must back that argument: singular homology API, circle $H_1$ computation, and the linking characterization already proved in DimensionForcing. It separates what is closed (API, object identity, linking iff, nonvanishing bridge) from what remains an external Mathlib computation target, without smuggling in the older concrete cohomology encoding.
Anyone tracing whether T8's cohomology dependence is fully discharged to Mathlib lands here first, then on the handoff certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.