linkingComplementH1
plain-language theorem explainer
For any continuous map f from the circle into the D-sphere, this is the first singular homology of the complement of its image, with integer coefficients, as a Mathlib ModuleCat object. It is the content-typed linking object that Alexander duality acts on. Anyone citing the non-encoding detector for spatial dimension will use it. The body is a direct application of Mathlib's singular homology functor to the complement subspace.
Claim. Given $D \in \mathbb{N}$ and a continuous map $f : S^1 \to S^D$, write $H_1(S^D \setminus \mathrm{im}(f);\mathbb{Z})$ for the first singular homology of the complement of the image of $f$, viewed as an object of the category of $\mathbb{Z}$-modules.
background
Recognition Science forces spatial dimension $D = 3$ (T8) by a linking obstruction: only in three dimensions can an embedded circle in the sphere have a homologically nontrivial complement. The object that carries that obstruction is ordinary singular homology of the complement, not an arithmetic encoding of linking numbers.
PublicSpine defines the content-typed linking object as first singular homology with $\mathbb{Z}$ coefficients of ${x \in S^D : x \notin \mathrm{range}(f)}$, obtained from Mathlib's singularHomologyFunctor. The present module restates that definition verbatim so the high-dimensional vanishing campaign can cite a local name. Upstream constants fix $D := 3$ as the forced spatial dimension; the detector predicate asks whether some embedding $f$ makes this homology module nonzero.
The construction lives in the TopCat / ModuleCat interface already present in Mathlib, so statements about it cannot be discharged by renaming or by empty detectors.
proof idea
Pure definition, no proof obligations. Form the complement subspace ${x : S^D \mid x \notin \mathrm{range}(f)}$ as a TopCat object, then apply Mathlib's singular homology functor in degree 1 with coefficients in the $\mathbb{Z}$-module $\mathbb{Z}$. The result is an object of ModuleCat $\mathbb{Z}$. Identical body to the PublicSpine and low-dimensional restatements.
why it matters
This is the Mathlib-native carrier for the linking half of the $D = 3$ forcing argument (T8 in the unified chain). Downstream, DetectsNontrivialLinking is literally the existence of an embedding $f : S^1 \hookrightarrow S^D$ for which this module is not the zero object; PublicSpine records that detector as panel K1 (non-encoding detector, corrected 2026-07-08) and notes that the detection half is proved in campaign P-d3link. The unknot-embedding theorem in UnknotComplementRetract also consumes the same shape when building the concrete $S^3$ witness. Without a genuine homology object, the dimension claim collapses to a name-firewall that empty predicates can inhabit. The high-dimensional module uses this def to state the frontier that arc complements are $H_1$-acyclic for $D \neq 3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.