linkingComplementH1
plain-language theorem explainer
Defines the first singular homology (integer coefficients) of the complement in S^D of the image of a continuous map from the circle. Anyone citing the low-dimension linking detector or the D=3 forcing argument uses this object. The body is a direct application of Mathlib's singular homology functor to the open complement subspace.
Claim. For each dimension $D \in \mathbb{N}$ and each continuous map $f : S^1 \to S^D$, let $H_1(S^D \setminus \mathrm{im}(f);\mathbb{Z})$ denote the first singular homology module (with $\mathbb{Z}$ coefficients) of the complement of the image of $f$ in the $D$-sphere. This is the content-typed linking object used by the nontrivial-linking detector.
background
This module is a Mathlib-only leaf that restates the public-spine linking object and detector, then proves the detector fails for $D=0$ and $D=1$. The object itself is the first singular homology of a circle complement in $S^D$: apply Mathlib's singularHomologyFunctor (coefficients in $\mathrm{Mod}(\mathbb{Z})$) in degree 1 to the topological space ${x \in S^D : x \notin \mathrm{range}(f)}$.
Upstream, the same definition appears in PublicSpine as the content-typed linking object: "First singular homology ($\mathbb{Z}$ coefficients, genuine Mathlib singularHomologyFunctor) of the complement of a continuous map from $S^1$ into $S^D$. This is the object Alexander duality computes." Parallel restatements live in the high-dimension leaf so each leaf can glue back to the spine by exact.
The detector built on top asks whether some embedded circle has non-vanishing $H_1$ of its complement. Spatial dimension $D=3$ is the value forced by the T8 step of the forcing chain; the low-dim leaf shows the detector is false for $D\in{0,1}$.
proof idea
Pure definition, not a proof. The body feeds the complement subspace
TopCat.of {x : sphere D // x ∉ range f}
into Mathlib's singular homology functor in degree 1 with $\mathbb{Z}$ coefficients, returning an object of ModuleCat ℤ. No lemmas are applied; the expression is the Mathlib object that later vanishing and non-vanishing arguments act on.
why it matters
This is the shared content type for the nontrivial-linking detector used across PublicSpine, the low-dim leaf, and the high-dim leaf. Downstream, DetectsNontrivialLinking is the proposition "there exists an embedding $f:S^1\hookrightarrow S^D$ whose complement has non-zero $H_1$"; the low-dim theorems not_detects_zero and not_detects_one show that proposition is false for $D=0,1$. The unknot-complement retract path also consumes the same shape when treating the standard unknot in $S^3$.
In the Recognition Science forcing chain, T8 forces spatial dimension $D=3$. The linking obstruction is the geometric reason: only in dimension 3 does an embedded circle have a homologically nontrivial complement in the sphere (Alexander duality / classical knot theory). By packaging the homology object as a genuine Mathlib singular-homology value rather than an arithmetic encoding, statements about it cannot be discharged by funext/propext tricks; they require actual homology of complements. The low-dim restatement exists so the vanishing proofs stay Mathlib-only and the parent spine can glue by definitional equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.