MathlibBackendHandoffCertificate
plain-language theorem explainer
A Prop package recording every obligation needed to hand T8's linking argument to Mathlib singular homology of the circle. Anyone citing the Mathlib-backed D=3 forcing path uses this certificate. It is a pure structure: fields pin the imported H_1(S^1;Z) object, the strong iso-to-Z interface, nonvanishing, and the backend that forces and supports dimension three.
Claim. A handoff certificate packs: the Mathlib cohomology bridge contract; the circle-$H_1$ target certificate; identity of the project circle homology with Mathlib's $H_1(S^1;\mathbb{Z})$; equivalence of a Mathlib $H_1$ computation with $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$; that iso (and a computation) imply nonvanishing; that a Mathlib circle-linking backend exists iff circle $H_1$ is nonzero, with constructors from nonvanishing, iso, and computation; and that any such backend agrees with the current linking predicate, forces $D=3$, and supports $D=3$.
background
The module sits at the Foundation layer that must replace a project-local encoding of circle cohomology by a genuine Mathlib singular-homology backend. Mathlib already exposes the singular homology functor on topological spaces with coefficients in $\mathbb{Z}$-modules, and the sphere object $S^1$. The missing piece for T8 is a computation of $H_1(S^1;\mathbb{Z})$ together with the Alexander-duality bridge from circle-complement homology to that group.
Spatial dimension in DimensionForcing is plain natural numbers. Nontrivial linking asks whether $S^D$ admits disjoint circle embeddings with nonzero linking number; by Alexander duality this holds precisely when $\tilde H_1(S^D\setminus S^1)\cong\tilde H^{D-2}(S^1)\cong\mathbb{Z}$, i.e. when $D=3$. The backend structure routes that predicate through nonvanishing of the concrete Mathlib circle homology object.
Upstream certificates already pin the imported object identity, the strong target $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, and the weaker nonvanishing target.
proof idea
No proof body: this is a structure definition (a bundled Prop). Each field is a named obligation. The first two fields embed the already-checked bridge contract and circle-$H_1$ target certificate. The rest are interface equalities and implications: object identity with Mathlib's functor on $S^1$; the iff between a filled Mathlib computation and the iso-to-$\mathbb{Z}$ proposition; nonvanishing arrows from iso and from computation; backend existence iff nonvanishing, with constructors from nonvanishing, iso, and computation; and linking-characterization fields that force agreement with SupportsNontrivialLinking, force $D=3$, and support $D=3$. The companion theorem later fills every field from existing lemmas.
why it matters
T8 in the forcing chain asserts that spatial dimension is three, via nontrivial linking of closed curves. The historical encoding used a project-local circle cohomology witness; this certificate is the paper-facing contract that the replacement must be the exact external Mathlib object $H_1(S^1;\mathbb{Z})$, not a local stand-in.
Downstream, the theorem mathlibBackendHandoffCertificate inhabits this structure, discharging every field from the bridge contract, the target certificate, and the circle-$H_1$ interface lemmas. Once a future Mathlib upgrade supplies the strong iso computation, the backend constructors here turn that single fact into a nonempty linking backend, which still forces and supports $D=3$.
The open gap the certificate isolates is precisely the missing Mathlib computation of circle homology; everything else in the T8 handoff is already pinned.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.