mathlibBackendHandoffCertificate
plain-language theorem explainer
A fully checked handoff certificate that the Mathlib singular-homology surface for the circle is wired into the T8 backend contract: the imported $H_1(S^1;\mathbb{Z})$ object, the strong isomorphism interface $H_1\cong\mathbb{Z}$, nonvanishing, and the linking backend that forces $D=3$. Anyone auditing the external Mathlib replacement path for dimension forcing would cite it. The proof is a structure assembly that plugs in already-proved field certificates.
Claim. There exists a paper-facing handoff certificate for the external Mathlib target: the cohomology-bridge contract holds; the circle $H_1$ target certificate is in place; the project's circle homology object equals Mathlib's singular homology of $S^1$ with $\mathbb{Z}$ coefficients; Mathlib computation is equivalent to $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$; that isomorphism (and the computation) imply nonvanishing; and the linking backend is equivalent to nonvanishing, is inhabited from either the iso or the computation, agrees with the current backend, forces $D=3$, and supports the $D=3$ linking story.
background
The module records the exact backend object needed to replace the project's concrete $S^1$ cohomology encoding for T8 (spatial dimension forcing). Mathlib already exposes the singular homology functor API, but the T8 replacement also needs a Mathlib-backed computation of the reduced cohomology of the circle and the Alexander-duality bridge from circle-complement homology to that group. The module deliberately does not fake the backend by reusing a project-local nontriviality lemma.
The handoff structure packages four layers: the bridge contract, a circle-$H_1$ target certificate on the pinned Mathlib surface, the strong interface $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (and its weaker nonvanishing shadow), and the backend object consumed by dimension forcing. Upstream, circleH1Z is definitionally Mathlib's singularHomologyFunctor at degree 1 on TopCat.sphere 1; the computation interface is proved equivalent to the iso-to-$\mathbb{Z}$ target; and nonvanishing follows from either the iso or the computation. Spatial dimension $D=3$ is the T8/T9 landmark the backend is meant to force via linking.
proof idea
Tactic-mode structure construction: each field of the handoff certificate is discharged by an already-proved sibling.
- Bridge contract: the module's
mathlibCohomologyBridgeContract. - Target certificate:
circleH1TargetCertificate(itself assembled from API availability, definitional equality to Mathlib homology, and the computation/iso/nonzero chain). - Target identity:
circleH1Z_is_mathlib_singular_homology(rflagainst the imported functor). - Computation $\leftrightarrow$ iso:
circleH1MathlibComputation_iff_iso_int. - Iso/computation $\Rightarrow$ nonzero: the two
circleH1ZNonzero_of_*lemmas. - Backend $\leftrightarrow$ nonzero and the three backend constructors: the
mathlibCircleLinkingBackend_*family. - Agreement, $D=3$ forcing, and $D=3$ support: projected from the backend witness fields (
agrees_with_current,forces_D3,d3_supports_linking).
No new algebraic work; pure certificate wiring.
why it matters
T8 in the forcing chain asserts $D=3$ spatial dimensions; the classical route uses nontrivial linking of $S^1$ in $\mathbb{R}^3$, which needs a trustworthy computation that $H_1(S^1;\mathbb{Z})$ is $\mathbb{Z}$ (or at least nonzero) and a backend that turns that into the linking/dimension statement. This handoff is the paper-facing seal that the external Mathlib singular-homology surface, not a local placeholder, is the object feeding that backend.
It sits at the end of the Mathlib cohomology bridge module: after the target certificate, the definitional import equality, and the computation/iso/nonzero equivalences have been established, this packages them with the linking backend constructors so a T8 replacement can cite one Prop. Downstream use is not yet recorded in the graph (used_by empty); the intended landing is whatever discharges the Mathlib-backed T8 path in DimensionForcing. Until a consumer theorem applies it, the certificate is an audited interface boundary rather than an in-line lemma in a larger proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.