MathlibCohomologyBridgeContract
plain-language theorem explainer
Packages the present-state contract for replacing the concrete circle-cohomology encoding by a Mathlib singular-homology backend. Auditors of the T8 dimension-forcing handoff cite it: the singular-homology API is import-checked, the working circle H1 object is pinned to Mathlib on the 1-sphere, linking holds exactly at D=3, and a Mathlib linking backend exists iff that H1 is nonzero. As a Prop structure it only lists fields; the inhabited instance is filled elsewhere from sibling certificates.
Claim. The Mathlib cohomology bridge contract holds when: (i) the singular homology functor API is available in the pinned Mathlib; (ii) the circle-$H_1$ target certificate holds (handoffs pinned to the imported object and to $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$); (iii) the working circle homology object equals Mathlib singular homology $H_1(S^1;\mathbb{Z})$; (iv) for every spatial dimension $D$, nontrivial linking of closed curves is supported iff $D=3$; (v) a Mathlib circle-linking backend exists if and only if that homology group is nonzero.
background
Mathlib already exposes the singular homology functor API, but the T8 replacement needs more: a Mathlib-backed computation of the reduced cohomology of $S^1$, plus the Alexander-duality bridge from circle-complement homology to that group. This module records the exact backend object required and deliberately refuses to fake it by reusing a prior concrete $S^1$ encoding.
Spatial dimension here is a natural number. Nontrivial linking is the genuine topological predicate: whether $S^D$ admits disjoint $S^1$-embeddings with nonzero linking number, fixed by Alexander duality ($\widetilde{H}_1(S^D\setminus S^1)\cong\widetilde{H}^{D-2}(S^1)\cong\mathbb{Z}$ iff $D=3$). The working circle homology object is Mathlib singular homology in degree 1 on the 1-sphere with $\mathbb{Z}$ coefficients. The Mathlib circle-linking backend is the future structure whose key field routes the $D=3$ linking characterization through nonvanishing of that concrete Mathlib object.
proof idea
Prop-valued structure definition, not a proved theorem. Its fields are the conjuncts of the contract: import-checked singular-homology API availability; the circle-$H_1$ target certificate (object pinned, strong iso-to-$\mathbb{Z}$ interface); definitional equality of the working object to Mathlib singular homology of $S^1$; the current linking characterization SupportsNontrivialLinking$(D)\leftrightarrow D=3$ from DimensionForcing; and the three implications relating nonemptiness of the Mathlib linking backend to nonvanishing of circle $H_1$. No tactics run at the structure itself. The separate inhabited instance fills each field from sibling lemmas and certificates.
why it matters
Feeds the paper-facing Mathlib backend handoff certificate, which packages the imported object, the strong $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ interface, the weaker nonvanishing target, and the backend object used by T8. It is inhabited by the checked contract theorem in the same module.
In the Recognition forcing chain, T8 forces three spatial dimensions via nontrivial linking of closed curves. This contract is the audit surface ensuring any replacement of the concrete $S^1$ encoding goes through Mathlib's singular homology functor rather than a hand-rolled stand-in. The open piece remains the actual Mathlib computation that $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ together with the Alexander-duality bridge that turns that nonvanishing into the $D=3$ linking characterization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.