circleH1Z_is_mathlib_singular_homology
plain-language theorem explainer
The project's named first homology of the circle equals Mathlib's singular homology H₁(S¹; ℤ) applied to the topological 1-sphere. Anyone auditing the Mathlib cohomology bridge cites this to confirm the target is the imported functor object, not a local stub. The proof is pure definitional equality (rfl).
Claim. The project's circle homology target equals the value of Mathlib's singular homology functor $H_1(-;\mathbb{Z})$ (as an object of $\mathbf{Mod}_{\mathbb{Z}}$) on the topological 1-sphere $S^1$.
background
The Mathlib Cohomology Bridge module records what external backend is still required before the project's concrete $S^1$ cohomology encoding can be retired. Mathlib already exposes the singular homology functor API; T8-style dimension forcing needs a genuine Mathlib computation of (reduced) circle homology/cohomology and an Alexander-duality link from circle-complement homology into that group.
The abbreviation circleH1Z is defined to be exactly
$((\mathrm{singularHomologyFunctor},\mathbf{Mod}_{\mathbb{Z}},1).\mathrm{obj},(\mathbb{Z})).\mathrm{obj},(S^1)$
in TopCat. Its doc-comment states the intent: "The concrete Mathlib object that must eventually be computed: first singular homology of the topological circle with integer coefficients."
This theorem is the identity check that the named target really is that imported object, not a project-local placeholder of the same type.
proof idea
One-line definitional proof: rfl. The left-hand side is an abbreviation whose body is literally the right-hand side Mathlib composite (singular homology functor in degree 1 with $\mathbb{Z}$ coefficients, evaluated on TopCat.sphere 1). No lemmas are applied.
why it matters
The bridge contract and handoff certificate both require an explicit check that the circle target is the imported Mathlib singular-homology object. Downstream, mathlibCohomologyBridgeContract records this equality as circle_h1_object_checked, and mathlibBackendHandoffCertificate records it as target_is_imported_circle_h1.
That certificate is the gate before replacing the current concrete $S^1$ cohomology encoding used on the path toward T8 (forcing $D=3$). The module deliberately refuses to fake the backend by reusing the older Alexander-duality nontriviality lemma; this identity pins the external target so later nonvanishing and linking obligations attach to the real Mathlib object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.