IndisputableMonolith.Foundation.MathlibCohomologyBridge
Import bridge certifying that the pinned Mathlib exposes the singular homology functor API (singular chains, short complexes, sphere objects). It is not the S¹ homology computation itself. Downstream circle-H₁ and T8 audit modules cite it as the real Mathlib surface any forced D=3 linking argument must eventually attach to.
claimThe pinned Mathlib provides the singular homology functor surface $H_n(-;\mathbb{Z})$ on topological spaces (via singular chains, module-category colimits, and short complexes), including the sphere objects $S^n$, so that a future identification $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ can be stated against real Mathlib types rather than a private model.
background
Recognition Science forces spatial dimension $D=3$ in the T8 step of the unified forcing chain. One classical route is topological: nontrivial linking and Alexander duality in three-space, which need a genuine computation of the first singular homology of the circle.
This module sits under Foundation and imports Mathlib's singular homology basics, ModuleCat colimits, short-complex homology, and TopCat spheres, together with the local DimensionForcing development. Its role is deliberately thin: record that the pinned Mathlib exposes that API, so later work does not invent a parallel homology theory.
Upstream, DimensionForcing frames the four arguments that force $D=3$, beginning with a topological linking argument. Downstream circle workbenches are expected to replace private chain models by Mathlib's imported singular homology object before feeding the strict T8 bridge.
proof idea
Definition and availability module, not a computation. It packages import-checked witnesses that the singular homology functor API is present, together with thin wrappers and predicates around a Mathlib-facing $H_1(S^1;\mathbb{Z})$ object (nonzero-ness, isomorphism to $\mathbb{Z}$, and a computation certificate type). No Alexander duality or full circle computation is proved here; those are deferred to consumer modules that must use this surface.
why it matters in Recognition Science
Without a real Mathlib attachment point, any $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ claim stays internal and cannot honestly support the topological half of T8 ($D=3$). This bridge is imported by CircleH1Computation (the local workbench for that missing isomorphism), by PublicSpine (the public dual forcing surface), and by T6T8SpineAudit (the honesty audit that tags what is theorem versus forced-conditional through T8).
It therefore anchors the foundation layer between Dimension Forcing and the audit spine: future proofs may close the circle computation only against this API, keeping the linking argument for $D=3$ from floating free of Mathlib.
scope and limits
- Does not prove $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
- Does not prove Alexander duality or any linking theorem in $\mathbb{R}^3$.
- Does not itself force $D=3$ or discharge T8.
- Does not replace `TopCat.sphere` models with a completed equivalence proof.
- Does not extend the Boolean UFC spine; it only exposes a Mathlib homology surface.
used by (3)
depends on (1)
declarations in this module (26)
-
def
MathlibSingularHomologyAPIAvailable -
theorem
mathlibSingularHomologyAPIAvailable -
abbrev
circleH1Z -
def
circleH1ZNonzero -
def
circleH1ZIsoInt -
structure
CircleH1MathlibComputation -
theorem
circleH1MathlibComputation_of_iso_int -
theorem
circleH1MathlibComputation_iff_iso_int -
theorem
intModuleCat_not_isZero -
theorem
circleH1ZNonzero_of_iso_int -
theorem
circleH1ZIsoInt_of_mathlib_computation -
theorem
circleH1ZNonzero_of_mathlib_computation -
structure
CircleH1TargetCertificate -
theorem
circleH1TargetCertificate -
theorem
circleH1Z_is_mathlib_singular_homology -
structure
MathlibCircleLinkingBackend -
def
mathlibCircleLinkingBackend_from_circleH1ZNonzero -
theorem
mathlibCircleLinkingBackend_nonempty_iff_circleH1ZNonzero -
theorem
circleH1ZNonzero_of_mathlibCircleLinkingBackend -
theorem
mathlibCircleLinkingBackend_of_circleH1ZNonzero -
theorem
mathlibCircleLinkingBackend_of_circleH1ZIsoInt -
theorem
mathlibCircleLinkingBackend_of_circleH1MathlibComputation -
structure
MathlibCohomologyBridgeContract -
theorem
mathlibCohomologyBridgeContract -
structure
MathlibBackendHandoffCertificate -
theorem
mathlibBackendHandoffCertificate