CircleH1TargetCertificate
plain-language theorem explainer
Certificate structure pinning every remaining circle first-homology handoff to Mathlib's singular homology of the circle and to the single strong target $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Cited by the Mathlib backend handoff and the cohomology-bridge contract that feed T8 dimension forcing. It is a Prop-structure definition packaging five interface obligations; it does not itself compute the homology group.
Claim. A certificate asserting: (1) Mathlib exposes the singular homology functor API; (2) the project's circle-$H_1$ object equals $((\mathrm{singularHomologyFunctor}(\mathrm{Mod}\,\mathbb{Z},1))(\mathbb{Z}))(S^1)$; (3) a filled Mathlib computation interface is inhabited if and only if $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ as $\mathbb{Z}$-modules; (4) that isomorphism implies the group is nonzero; (5) any such computation implies nonvanishing.
background
This module records the exact Mathlib backend needed to replace a project-local $S^1$ cohomology encoding used on the path to T8 ($D=3$ spatial dimensions). Mathlib already supplies the singular homology functor API; what is still missing is a pinned computation of $H_1(S^1;\mathbb{Z})$ and the Alexander-duality bridge from circle-complement homology.
The concrete target object circleH1Z is defined as the value of Mathlib's singular homology functor at degree 1 on the topological circle with integer coefficients. The strong closure goal is an isomorphism of that object with $\mathbb{Z}$ as a $\mathbb{Z}$-module; the weaker goal is mere nonvanishing (not the zero object in $\mathrm{Mod},\mathbb{Z}$).
MathlibSingularHomologyAPIAvailable is only the import-checked fact that the functor surface exists. CircleH1MathlibComputation is the final import interface: API available, target identity, and the iso-to-$\mathbb{Z}$ field. The present structure packages those pieces into a single checked handoff certificate without filling the missing computation.
proof idea
No proof body: this is a Prop-structure definition. Its five fields are pure interface obligations. The inhabited instance is built downstream by circleH1TargetCertificate, which fills them via the API availability lemma, definitional equality (rfl) for the target identity, the iff between the computation interface and iso-to-$\mathbb{Z}$, and the two nonvanishing implications from iso and from any computation witness.
why it matters
Pins the circle-$H_1$ surface so later certificates cannot silently swap in a project-local stand-in. Downstream, circleH1TargetCertificate constructs an instance; MathlibCohomologyBridgeContract requires this certificate alongside the API check; MathlibBackendHandoffCertificate packages it into the paper-facing handoff that names the external Mathlib target, the strong iso interface, the weaker nonvanishing target, and the backend object used by T8.
In the forcing chain, T8 forces three spatial dimensions; the classical route uses nontrivial reduced cohomology of $S^1$ (or an Alexander-duality bridge from circle complements). This certificate keeps that dependency honest: every remaining handoff is locked to Mathlib's $H_1(S^1;\mathbb{Z})$ and to $\cong\mathbb{Z}$, while the actual homology computation stays an open Mathlib-backed obligation rather than a faked local encoding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.