mathlibCircleLinkingBackendOfGeometricBridge
plain-language theorem explainer
Assuming a chain-homotopy equivalence between Mathlib singular chains on S¹ and the ordinary two-cell cellular circle model, one obtains a nonempty Mathlib circle-linking backend. Anyone wiring singular H₁(S¹;ℤ)≅ℤ into the cohomology bridge cites this. The proof is a one-line composition: geometric bridge implies the ℤ-iso, which builds the backend.
Claim. If Mathlib's singular chain complex on $\mathrm{TopCat.sphere}\,1$ is chain-homotopy equivalent to the ordinary two-cell cellular circle model, then the Mathlib circle-linking backend structure is inhabited (nonempty).
background
This module is the local workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not yet replace Mathlib's TopCat.sphere 1 singular homology object in the strict T8 bridge; it only prepares algebraic and geometric atoms toward that closure.
The geometric bridge is the remaining chain-level hypothesis: a nonempty chain-homotopy equivalence between Mathlib's singular integer chain complex on the 1-sphere and the ordinary cellular circle model (two cells). From that equivalence one already obtains the exact interface proposition circleH1ZIsoInt used by the cohomology bridge ("the geometric bridge immediately closes the exact proposition used by MathlibCohomologyBridge").
The Mathlib circle-linking backend is the structure that must replace the concrete $S^1$ cohomology encoding. Its key obligations include nonvanishing of the concrete Mathlib circle homology object and a linking map routed through that computation, under a singular-homology API availability flag.
proof idea
One-line term wrapper. Apply circleH1ZIsoIntOfGeometricBridge to the geometric-bridge hypothesis to obtain circleH1ZIsoInt. Feed that iso into mathlibCircleLinkingBackend_of_circleH1ZIsoInt, which builds a nonempty MathlibCircleLinkingBackend by first deriving nonvanishing of $H_1$ from the iso and then packaging the backend fields. No extra algebraic work occurs at this site.
why it matters
In the Recognition foundation stack this declaration is the last glue step from the geometric chain-level bridge to the Mathlib linking backend object required by the cohomology bridge. The module doc is explicit that the workbench does not yet feed the strict T8 bridge (D = 3 spatial dimensions) until a real equivalence to Mathlib's imported singular homology is proved; the geometric bridge is precisely that remaining hypothesis, and this theorem shows it is already enough to inhabit the backend.
Downstream use is not yet recorded in the graph (zero used_by edges). The parent conceptual consumer is the Mathlib cohomology bridge's linking path: once the backend is nonempty, linking can be routed through the computed circle $H_1$ rather than a hand-rolled encoding. The algebraic core (degree-1 single $\mathbb{Z}$ complex has $H_1\cong\mathbb{Z}$) is already proved in-module; this result only packages the geometric hypothesis into the backend interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.