circleH1ZNonzero_of_mathlibCircleLinkingBackend
plain-language theorem explainer
If a Mathlib circle-linking backend exists, then the first singular homology of the circle with integer coefficients is nonvanishing. Anyone wiring the T8 dimension-forcing argument to Mathlib singular homology cites this projection. The proof is a one-line application of the forward half of the backend-nonempty equivalence.
Claim. If there exists a Mathlib circle-linking backend (a package that exposes the singular-homology API, asserts $H_1(S^1;\mathbb{Z})\neq 0$, and routes the linking support predicate through that nonvanishing), then the concrete Mathlib object $H_1(S^1;\mathbb{Z})$ is not the zero module.
background
The module is the Mathlib cohomology bridge contract for T8. Mathlib already exposes the singular homology functor API, but replacing the hand-rolled $S^1$ cohomology encoding needs a Mathlib-backed computation of the circle's first homology together with an Alexander-duality route from circle-complement homology into that group. The module deliberately refuses to fake that backend by recycling the older concrete nonvanishing certificate.
Here circleH1Z is the Mathlib singular homology object $H_1(S^1;\mathbb{Z})$, and circleH1ZNonzero is the proposition that this object is not the zero object in the module category. The backend structure MathlibCircleLinkingBackend packages four fields: a dimension-support predicate, a witness that the singular-homology API is available, the nonvanishing fact itself, and a linking law that forces support exactly when the ambient dimension is $3$ and the circle homology is nonzero.
Upstream, the equivalence mathlibCircleLinkingBackend_nonempty_iff_circleH1ZNonzero records that inhabiting the backend is logically the same as proving the single concrete nonvanishing computation.
proof idea
One-line term proof. Apply the forward direction (.mp) of the already-proved equivalence mathlibCircleLinkingBackend_nonempty_iff_circleH1ZNonzero, which states Nonempty MathlibCircleLinkingBackend ↔ circleH1ZNonzero. The hypothesis supplies the left-hand side; the equivalence yields the right-hand side. No further case analysis or homology computation is performed here.
why it matters
This is the projection half of the backend contract that will eventually replace the concrete $S^1$ cohomology encoding used in dimension forcing. In the Recognition Science chain, T8 forces $D=3$ spatial dimensions; the linking characterization inside the backend routes that force through Mathlib's $H_1(S^1;\mathbb{Z})$ rather than a bespoke certificate. The companion reverse direction builds a backend from the nonvanishing fact, so together the two theorems collapse the entire backend obligation to a single Mathlib homology computation.
No downstream consumers are wired yet (used_by is empty). The declaration sits ready for the T8 replacement path once Mathlib supplies (or the project proves) the concrete isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ and the Alexander-duality bridge named in the module header.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.