mathlibSingularHomologyAPIAvailable
plain-language theorem explainer
Import-checked witness that Mathlib exposes the singular homology functor API for every admissible coefficient category and degree. Bridge authors replacing the T8 circle-cohomology backend cite it as the real Mathlib surface those computations must use. The proof is a one-line packing of Mathlib's functor with reflexivity.
Claim. For every category $C$ with coproducts, a preadditive structure, and homology, and for every degree $n\in\mathbb{N}$, the Mathlib singular homology functor of degree $n$ with coefficients in $C$ exists as a functor $C\to\mathrm{Fun}(\mathbf{Top},C)$ and equals Mathlib's `singularHomologyFunctor`.
background
The module records a contract for replacing the current concrete $S^1$ cohomology encoding by a Mathlib-backed backend. Mathlib already supplies the singular homology functor API; the T8 replacement still needs a computation of the reduced cohomology of the circle and an Alexander-duality bridge from circle-complement homology to that group.
The proposition being proved is the import-checked availability statement: for every coefficient category $C$ (with the usual categorical hypotheses) and every $n$, there is a nonempty subtype of functors equal to Mathlib's singular homology functor of degree $n$. It is deliberately not the $S^1$ computation itself and not Alexander duality; it only certifies the real Mathlib surface those future results must use.
Local setting is the Foundation forcing chain, where T8 forces $D=3$ spatial dimensions and the eight-tick octave. Circle homology nonvanishing is the linking ingredient that backend must eventually supply.
proof idea
Term-mode proof. Introduce the coefficient category $C$, its categorical instances, and the degree $n$. Return the pair consisting of Mathlib's AlgebraicTopology.singularHomologyFunctor C n together with rfl, which inhabits the nonempty subtype demanded by the proposition. No auxiliary lemmas are needed beyond the imported Mathlib definition.
why it matters
This is the first checked field of the Mathlib cohomology bridge contract. Downstream, circleH1MathlibComputation_of_iso_int packages it with a proof that $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ to fill the strong computation interface; circleH1TargetCertificate records the full target certificate; mathlibCircleLinkingBackend_from_circleH1ZNonzero builds the T8 linking backend once circle $H_1$ nonvanishing is known; and mathlibCohomologyBridgeContract assembles the remaining replacement contract.
In the Recognition forcing chain, T8 forces $D=3$ and the eight-tick period. The missing Mathlib piece is a genuine computation of circle homology (plus Alexander duality), not a recycled internal nontriviality lemma. This theorem locks the API surface so that future work cannot fake the backend.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.