DetectsNontrivialLinking
plain-language theorem explainer
A dimension D admits nontrivial linking when some topologically embedded circle in the D-sphere has nonvanishing first singular homology of its complement. Recognition Science cites this predicate when forcing spatial dimension three from the existence of linked loops (forcing chain T8). The body is a pure existence Prop over continuous embeddings and the singular-homology functor; no proof obligation attaches.
Claim. For a natural number $D$, the predicate holds if and only if 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 object in the category of $\mathbb{Z}$-modules.
background
The module LinkingVanishingHighDim packages the high-dimensional half of the Alexander linking argument that forces spatial dimension three in the Recognition Science forcing chain (T8 / T9). The companion low-dimensional module already rules out $D=0$ and $D=1$ unconditionally.
The auxiliary object linkingComplementH1 takes a continuous map $f:S^1\to S^D$ and returns the first singular homology (integer coefficients) of the open complement of the image of $f$ inside the $D$-sphere, realized as an object of ModuleCat $\mathbb{Z}$. Nonvanishing of that module is the homological signature of nontrivial linking.
Upstream, the constant $D:=3$ appears in AlphaDerivation and GapDerivation as the spatial dimension forced by linking. The remaining classical input is ArcComplementsAcyclic: every topological embedding of the unit interval into $S^D$ has $H_1$-acyclic complement (Hatcher 2B.1, arc case); the file consumes that statement as a hypothesis parameter.
proof idea
Definitional unpacking only. The predicate is the existential statement that there exists a continuous map $f$ from the 1-sphere to the $D$-sphere which is a topological embedding and for which the first singular homology of the complement fails to be the zero object in ModuleCat $\mathbb{Z}$. The zero test is Mathlib's IsZero. No lemmas are applied; the body is a pure Prop constructor restating the PublicSpine interface.
why it matters
This predicate is the detection side of the Alexander linking bridge that pins spatial dimension to three (forcing chain T8). Downstream, not_detects_of_arcAcyclic shows that under ArcComplementsAcyclic, no dimension $D\ge 1$ with $D\ne 3$ satisfies the predicate. The uniqueness half forces_D3_of_arcAcyclic then concludes that any $D$ detecting nontrivial linking must equal 3, once arc acyclicity is granted for all other dimensions at least 2.
PublicSpine.AlexanderLinkingBridge consumes the same predicate as the public interface. Low-dimensional siblings already prove the negation for $D=0$ and $D=1$ without hypotheses. The open classical frontier is precisely ArcComplementsAcyclic for $D\ge 2$, $D\ne 3$; closing that frontier discharges the conditional uniqueness theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.