DetectsNontrivialLinking
plain-language theorem explainer
Predicate on a dimension D: some embedded circle in the D-sphere has complement with nonvanishing first integer homology. This is the content-typed linking detector for the T8 spatial-dimension argument (panel K1). Pure Prop definition packing an embedding plus a non-zero H₁ of the complement; no proof content.
Claim. For $D \in \mathbb{N}$, the assertion that there exists a continuous embedding $f : S^1 \hookrightarrow S^D$ such that the first singular homology $H_1(S^D \setminus \mathrm{im}(f);\mathbb{Z})$ is not the zero module in $\mathbf{Mod}_{\mathbb{Z}}$.
background
PublicSpine is the dual forcing surface to UnifiedForcingChain: δ-stratified claims papers should cite for what is forced, including the closed D=3 / eight-tick bridge (campaign P-d3link). The detector here is the honest binder for nontrivial circle linking in a sphere.
The first homology of the complement is computed by Mathlib singular homology on the subspace of $S^D$ outside the image of $f$. Upstream, $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$ holds unconditionally (circleH1ZIsoInt_holds). The classical unknot $z \mapsto (z,0,0)$ in $S^3$ has complement retracting onto a core circle, so that isomorphism witnesses nonvanishing at $D=3$.
Earlier abstract detects : ℕ → Prop binders were gameable (empty detector, or equal by funext/propext to an encoding predicate). Content-typing on the Mathlib objects is the non-gameable form (panel K1).
proof idea
Definitional Prop, not a proved theorem. The body is the existential package: a continuous map $f$ from the 1-sphere to the $D$-sphere that is a topological embedding, together with the assertion that linkingComplementH1 D f (singular $H_1$ of the open complement, as a $\mathbb{Z}$-module) is not a zero object in the module category. No tactics or lemmas fire at this site; inhabitation and vanishing live in the low-dim and high-dim linking modules.
why it matters
This binder is the shared interface for the Alexander linking bridge that closes T8 ($D=3$ spatial dimensions) on the public spine. Low-dim modules prove it fails at $D=0,1$; high-dim modules prove (conditional on arc-complement $H_1$-acyclicity) it fails for $D=2$ and $D\ge 4$, and that detection forces $D=3$ (forces_D3_of_arcAcyclic, not_detects_of_arcAcyclic). The $D=3$ positive half uses the unknot complement retract and the unconditional circle homology isomorphism.
Module contract: T8/T7 must cite this content-typed detector (via AlexanderLinkingBridge), never an arithmetic encoding predicate. Downstream restatements in LinkingVanishingLowDim and LinkingVanishingHighDim keep the same Prop so vanishing and uniqueness theorems speak the public language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.