circleH1TargetCertificate
plain-language theorem explainer
Packages a checked certificate that the project's circle first-homology target is exactly Mathlib's singular homology $H_1(S^1;\mathbb{Z})$, with every remaining handoff pinned to the single strong goal $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Downstream bridge-contract and backend-handoff theorems cite it. The proof is a structure inhabitant: five fields filled by prior lemmas and `rfl`.
Claim. There is a checked certificate asserting: Mathlib's singular homology functor API is available; the project's circle first-homology object equals Mathlib's $H_1(S^1;\mathbb{Z})$; a Mathlib computation of that group is equivalent to an isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$; and either such an isomorphism or such a computation implies the group is nonzero.
background
The Mathlib Cohomology Bridge module records the exact backend needed to replace a project-local $S^1$ cohomology encoding used in the T8 dimension-forcing path. Mathlib already exposes the singular homology functor API, but the replacement still needs a Mathlib-backed computation of $H_1(S^1;\mathbb{Z})$ (and later an Alexander-duality bridge from circle-complement homology).
The certificate structure does not itself compute homology. Its fields pin: availability of Mathlib's singular homology functor; definitional equality of the project's circleH1Z with ((singularHomologyFunctor (ModuleCat $\mathbb{Z}$) 1).obj (ModuleCat.of $\mathbb{Z}$ $\mathbb{Z}$)).obj (TopCat.sphere 1); equivalence of a nonempty Mathlib-computation interface with an isomorphism to $\mathbb{Z}$; and the two nonvanishing implications from that isomorphism or computation.
Upstream, mathlibSingularHomologyAPIAvailable witnesses the functor exists; circleH1MathlibComputation_iff_iso_int equates the computation interface with $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$; and the two circleH1ZNonzero_of_* lemmas close nonvanishing once the iso or computation is in hand.
proof idea
Term-mode structure constructor for CircleH1TargetCertificate. Each field is discharged by an existing fact:
- singular-homology API:
mathlibSingularHomologyAPIAvailable; - target equals imported Mathlib circle $H_1$:
rfl(definitional); - computation interface $\leftrightarrow$ iso to $\mathbb{Z}$:
circleH1MathlibComputation_iff_iso_int; - iso implies nonzero:
circleH1ZNonzero_of_iso_int; - computation implies nonzero:
circleH1ZNonzero_of_mathlib_computation.
No new algebraic work; pure packaging of the pinned handoff surface.
why it matters
This is the final circle-$H_1$ target certificate on the pinned Mathlib surface. It feeds directly into mathlibCohomologyBridgeContract ("checked contract for the remaining Mathlib cohomology replacement") and mathlibBackendHandoffCertificate ("checked handoff certificate for the exact external Mathlib target").
In the Recognition forcing chain, T8 forces $D=3$ spatial dimensions; the cohomology bridge is the Mathlib-backed replacement path for the concrete $S^1$ cohomology encoding that path uses. The certificate deliberately refuses to fake the backend via the older project-local nontriviality lemma: every remaining handoff is locked to Mathlib's singular homology of the 1-sphere and to the single strong target $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
What remains open is the actual Mathlib computation of that group (and the Alexander-duality bridge named in the module doc). This declaration only certifies that the interface is correctly aimed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.