mathlibCircleLinkingBackend_unconditional
plain-language theorem explainer
The Mathlib circle-linking backend exists unconditionally: singular H₁ of the circle is nonzero, so the structure that routes linking through Mathlib homology is inhabited. Anyone closing the T8 dimension-forcing chain or replacing project-local S¹ cohomology cites this. The proof is a one-line application of the backend constructor to the already-proved nonvanishing theorem.
Claim. There exists a Mathlib circle-linking backend: a package witnessing that singular homology $H_1(S^1;\mathbb{Z})$ is nonzero and that linking numbers, for admissible dimensions, can be read off that Mathlib computation.
background
This module lifts the path-level winding/displacement invariant on $S^1$ to singular $1$-simplices and proves that displacement kills boundaries of $2$-simplices. That chain-level identity, together with the fact that the once-around loop has winding $1$, yields a winding homomorphism on $1$-cycles that is a left inverse of the fundamental class: the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The Mathlib circle-linking backend is the structure that replaces project-local $S^1$ cohomology encodings. Its decisive field is nonvanishing of the concrete Mathlib object circleH1Z (definitionally the degree-$1$ singular homology of the sphere), plus a routing of linking through that computation and a witness that the singular-homology API is available.
Upstream, circleH1ZNonzero_unconditional discharges that nonvanishing: it reduces to homologyOne_nonzero via the isomorphism identifying the bridge object with Mathlib's singular homology of the circle. A separate constructor turns any such nonvanishing proof into a nonempty backend.
proof idea
One-line term wrapper. Apply the constructor that builds a nonempty backend from any proof of circle-$H_1$ nonvanishing, feeding it the unconditional nonvanishing theorem already established in this module. No further case analysis or simplicial work is required at this step.
why it matters
This is the unconditional existence of the Mathlib linking backend that the foundation layer needs once project-local circle cohomology is retired. The strict T1-to-T8 frontier only demands nonvanishing of $H_1(S^1;\mathbb{Z})$; that nonvanishing is already proved, and this declaration packages it into the backend structure used for dimension forcing and linking.
The module doc is explicit that full generation (every degree-$1$ class is an integer multiple of the fundamental class, i.e. surjectivity of the comparison map $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$) is stronger and not required for T8 closure. No downstream consumers are wired yet in the graph; the declaration stands as the discharged interface point for any later linking or dimension-forcing argument that imports the Mathlib backend.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.