mathlibCircleLinkingBackend_holds
plain-language theorem explainer
The Mathlib circle-linking backend exists as a nonempty structure, with no remaining hypotheses. Dimension-forcing and T8 work cite this to replace project-local S¹ cohomology encodings by Mathlib singular homology. The proof is a one-line application of the zero-winding-bound constructor to the unconditional free-prism generation theorem.
Claim. There exists a Mathlib circle-linking backend: a package that supplies singular-homology API availability, nonvanishing of $H_1(S^1;\mathbb{Z})$, and a linking map from that computation into the dimension-forcing interface.
background
The ambient module lifts path-level winding on $S^1$ to singular $1$-simplices. Displacement of a singular $1$-simplex is path displacement after reparameterizing $\Delta^1$ to the unit interval; the key identity is that alternating face sums of displacements vanish on every singular $2$-simplex (winding kills boundaries). Together with the fact that the once-around loop has winding $1$, this yields a left inverse to the fundamental class on $H_1(S^1;\mathbb{Z})$.
The structure being inhabited is the bridge backend that routes linking through Mathlib's singular homology rather than a project-local circle encoding. Its fields demand a usable singular-homology API, a proof that circle $H_1$ is nonzero, and a linking map from that object into the dimension-forcing layer.
Upstream, the zero-winding cycles bound asserts every singular $1$-cycle of winding zero is a boundary; that bound is already proved unconditionally via free-prism generation of oriented cyclic families. A prior constructor turns any such bound into a nonempty backend.
proof idea
One-line term proof. Apply the constructor that builds a nonempty Mathlib circle-linking backend from a zero-winding cycles bound, feeding it the already-proved unconditional zero-winding bound (itself obtained by transporting free-prism generation of oriented cyclic families across the corresponding iff). No further case analysis or cohomology computation appears at this site.
why it matters
Strict T8 dimension replacement requires an unconditional Mathlib circle-linking backend; this theorem discharges that obligation. Downstream it is consumed by the public T-2-to-T8 forcing certificate, which packages the full chain (including circle $H_1$ nonvanishing and the integer isomorphism) as theorem-backed rather than hypothesis-gated. In the Recognition forcing ladder this closes the homology half of the $D=3$ step: linking and nonvanishing no longer depend on a stubbed or project-local $S^1$ model. The generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ still leans on prism/subdivision infrastructure already internalized here via free prisms; no open scaffold remains on this edge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.