CircleH1MathlibComputation
plain-language theorem explainer
Final Mathlib handoff certificate for first singular homology of the circle: Mathlib's singular-homology functor is in scope, the project's circle-H1 object is exactly that functor on S^1 with integer coefficients, and the result is isomorphic to Z. T8 and circle-bridge theorems cite this as the single strong computation interface. As a Prop structure it has no proof body; inhabitants are assembled once the isomorphism is known, with API and target identity already import-checked.
Claim. The Mathlib circle-$H_1$ computation interface holds when (i) Mathlib exposes the singular homology functor API, (ii) the project's circle first-homology object equals $H_1^{\mathrm{sing}}(S^1;\mathbb{Z})$ as given by that functor on the topological 1-sphere, and (iii) there is an isomorphism $H_1^{\mathrm{sing}}(S^1;\mathbb{Z})\cong\mathbb{Z}$ in $\mathbb{Z}$-modules.
background
This module is the Mathlib cohomology bridge contract. Mathlib already exposes the singular homology functor API, but the T8 dimensional-forcing replacement needs a Mathlib-backed computation of circle homology/cohomology, plus an Alexander-duality bridge from circle-complement homology. The module deliberately does not fake that backend by reusing a project-local nontriviality lemma.
The API-availability predicate records that, for suitable coefficient categories $C$, Mathlib supplies singularHomologyFunctor C n. The circle first-homology abbreviation is exactly that functor at degree 1 with $\mathbb{Z}$ coefficients applied to the topological 1-sphere. The strong target is nonemptiness of an isomorphism from that object to the free rank-one $\mathbb{Z}$-module.
proof idea
No proof body: this is a Prop-valued structure (definitional interface). An inhabitant is a triple of field proofs. The companion constructor from the strong isomorphism builds one by filling the API field with the already-checked import fact and the target-identity field by reflexivity; the converse projection recovers the isomorphism from any inhabitant. Equivalence of inhabitation with the bare iso is proved by those two directions.
why it matters
This is the final import interface the T8 handoff waits on. Downstream, the geometric-bridge theorem fills the certificate from a geometric iso; extractors recover the strong iso and the nonvanishing statement; the target and backend handoff certificates pin every remaining circle-H1 edge to the imported Mathlib object and to $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Equivalence with the bare iso means the only missing mathematical content is Mathlib's actual computation of that group. Filling it from pinned Mathlib (not a project-local stand-in) is the open path to replace the current concrete $S^1$ cohomology encoding in the dimension-forcing chain (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.