DetectsNontrivialLinking
plain-language theorem explainer
Predicate on a natural number D: some continuous embedding of the circle into the D-sphere has nonvanishing first singular homology on its complement. Low-dimension vanishing theorems cite it to rule out D = 0 and 1; the high-dimension bridge uses the same predicate to force D = 3 under arc acyclicity. Definitional restatement of the PublicSpine detector, packaged for Mathlib-only gluing by exact.
Claim. For $D \in \mathbb{N}$, the predicate holds iff there exists a continuous embedding $f : S^1 \hookrightarrow S^D$ such that the first singular homology $H_1(S^D \setminus f(S^1); \mathbb{Z})$ is a nonzero $\mathbb{Z}$-module.
background
This module is a Mathlib-only leaf that restates the content-typed linking detector from PublicSpine and proves it fails for $D = 0$ and $D = 1$. The companion object linkingComplementH1 is the first singular homology (coefficients in $\mathbb{Z}$) of the complement of the image of a continuous map $f : S^1 \to S^D$ inside the $D$-sphere.
The detector packages existence of an embedding whose complement homology is non-zero. That is the topological content of nontrivial linking in the Alexander sense: the circle is knotted into $S^D$ so that loops in the complement survive in $H_1$. Upstream constants fix spatial dimension $D = 3$ by the forcing chain (T8); this predicate is the bridge object those uniqueness arguments quantify over.
Universes and implicit arguments match the parent PublicSpine and the high-dimension twin module, so parent theorems can glue by exact without re-proving the Prop shape.
proof idea
Definitional: the body is the existential Prop itself. No tactics. It asserts existence of a continuous map $f$ from the topological 1-sphere to the $D$-sphere that is a topological embedding and for which linkingComplementH1 D f is not the zero object in ModuleCat ℤ. The high-dimension twin restates the identical Prop for the arc-acyclicity half of the bridge.
why it matters
Local consumers are not_detects_zero and not_detects_one, which discharge the detector in dimensions 0 and 1 unconditionally (finite totally disconnected 0-sphere; surjective self-embeddings of $S^1$ leave empty complement). Downstream, forces_D3_of_arcAcyclic and not_detects_of_arcAcyclic quantify over the same predicate: granting arc-complement $H_1$-acyclicity for every $D \ge 2$, $D \ne 3$, nontrivial linking forces $D = 3$. PublicSpine's Alexander linking bridge also depends on it.
In the Recognition forcing chain this is the topological half of T8 (spatial dimension three): linking is detectable only when the ambient sphere dimension permits nontrivial circle complements. Dimensions 0 and 1 are banked here; the remaining uniqueness is conditional on the arc frontier in the high-dimension module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.