IndisputableMonolith.Foundation.LinkingVanishingLowDim
Low-dimensional half of the linking-vanishing story for Recognition Science: first homology of a linking complement cannot detect nontrivial linking in dimensions 0 and 1. Restates the public-spine claim and packages the classical continuum facts (no continuous injection of the circle into the line; continuous injective circle self-maps are surjective). Cited by the dual forcing surface and by the high-dimensional companion module. Content is elementary topology, not a deep algebraic argument.
claimLow-dimensional linking vanishing: $H_1$ of a linking complement does not detect nontrivial linking in dimensions $0$ and $1$. Equivalently, there is no continuous injective map $S^1\to\mathbb{R}$, and every continuous injective self-map of $S^1$ is surjective.
background
PublicSpine is the public dual of UnifiedForcingChain: a $\delta$-stratified forcing surface that keeps the Boolean certificate spine for pedagogy while exposing the honest cut between the $\delta$-only tower $(\mathbb{N}/\mathbb{Z}/\mathbb{Q})$ and the continuum extension. Linking of cycles is read off nontriviality of the first singular homology of the complement.
This module isolates the low-dimensional half of that detection story. The supporting facts are classical continuum topology: the circle does not embed continuously into the real line (removing a point disconnects $S^1$ but not $\mathbb{R}$ in the same way), and a continuous injective endomorphism of $S^1$ is surjective by compactness. Finite-type lemmas about one-dimensional spheres appear as auxiliaries.
Mathlib imports supply singular homology, module categories, short complexes, and sphere instances so the $H_1$-of-complement language matches the high-dimensional companion.
proof idea
Restatement layer for the public-spine linking-complement-$H_1$ claim, together with the elementary topological lemmas that close dimensions 0 and 1. The non-detection statements reduce to: no continuous injection $S^1\to\mathbb{R}$, and continuous injective self-maps of $S^1$ are surjective. Both are standard connectedness/compactness arguments; the module only packages them under the DetectsNontrivialLinking predicate and the linkingComplementH1 interface. No spectral sequence or higher homotopy is used here.
why it matters in Recognition Science
Imported by LinkingVanishingHighDim (high-dimensional companion) and by PublicSpine, the dual forcing surface of UnifiedForcingChain. PublicSpine's doc fixes the contract: $\delta$-only tower on $\mathbb{N}/\mathbb{Z}/\mathbb{Q}$, continuum cut via classicalExtension, without placing $\neg\mathbb{R}$ under deltaOnly. Low-dimensional linking vanishing is the base case that keeps that dual surface honest when ambient dimension is too small for nontrivial linking to appear in $H_1$ of the complement. Without it the spine would carry an unstated gap at dim $\le 1$.
scope and limits
- Does not treat linking detection in dimension ≥ 2 (that is LinkingVanishingHighDim).
- Does not claim vanishing of higher homology groups H_k for k > 1.
- Does not replace or delete UnifiedForcingChain; only supports the dual PublicSpine surface.
- Does not assert choice-sensitive continuum pathologies beyond classical facts about R and S^1.
- Does not define the full δ-stratified tower; that lives in PublicSpine.