MathlibCircleLinkingBackend
plain-language theorem explainer
Interface package for a Mathlib-backed S¹ linking backend that forces spatial dimension three. Anyone replacing the concrete circle-cohomology encoding in the T8 dimension-forcing chain cites this contract. It is a pure structure: four fields that pin singular-homology API availability, nonvanishing of H₁(S¹;ℤ), and the iff that linking support holds exactly when D=3 and that H₁ is nonzero.
Claim. A Mathlib circle-linking backend is a package consisting of: a predicate $P$ on spatial dimensions; a witness that Mathlib exposes the singular homology functor API; a witness that $H_1(S^1;\mathbb{Z})$ is nonzero; and a proof that for every dimension $D$, $P(D)$ holds if and only if $D=3$ and $H_1(S^1;\mathbb{Z})\neq 0$.
background
The module records the exact backend object needed to replace the current concrete $S^1$ cohomology encoding used by T8 (spatial dimension forcing). Mathlib already supplies the singular homology functor API, but T8 replacement needs a Mathlib-backed computation of the reduced cohomology of the circle, plus the Alexander-duality bridge from circle-complement homology to that group.
MathlibSingularHomologyAPIAvailable is only the import-checked fact that the pinned Mathlib exposes singularHomologyFunctor; it is not yet the $S^1$ computation. Sibling targets circleH1ZNonzero and circleH1ZIsoInt name the concrete nonvanishing and $\mathbb{Z}$-isomorphism goals for $H_1(S^1;\mathbb{Z})$. Dimension here is the discrete spatial dimension from DimensionForcing, not the $[L,T,M]$ signature structure.
The module deliberately refuses to fake the backend by reusing the existing AlexanderDuality.CircleReducedCohomologyNontrivial encoding.
proof idea
No proof: this is a structure definition. The four fields are the contract. Downstream lemmas on the structure are one-line wrappers: circle_linking_iff projects the linking field to drop the redundant $H_1$ conjunct (using the stored nonvanishing witness); agrees_with_current equates the backend predicate with SupportsNontrivialLinking via D3_has_linking and linking_requires_D3; forces_D3 and d3_supports_linking are the two directions of that iff specialized to the forcing statement.
why it matters
This is the T8 replacement surface. The forcing chain step T8 asserts $D=3$ spatial dimensions from nontrivial linking; the old path used a hand-rolled circle cohomology encoding. Any Mathlib-native replacement must inhabit this structure so that linking still characterizes exactly $D=3$, but now routed through concrete $H_1(S^1;\mathbb{Z})$ nonvanishing.
Downstream, CircleWindingChain builds inhabitants from winding-map mono, cyclic edge-list decompositions, extraction steps, and zero-winding bounds, culminating in the unconditional existence theorem mathlibCircleLinkingBackend_holds required by the strict T8 dimension replacement. CircleH1Computation.mathlibCircleLinkingBackendOfGeometricBridge likewise constructs the backend from the geometric bridge. Closing those chains discharges the Mathlib cohomology bridge contract without faking the $S^1$ computation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.