detectsNontrivialLinking_three
plain-language theorem explainer
In dimension three, some embedded circle in the 3-sphere has homologically nontrivial complement: the flat unknot works. Anyone citing the non-encoding D=3 linking half of the Alexander bridge needs this fact. The proof is a short term package: unknot embedding plus complement retract onto a core circle, so nontrivial H₁(S¹;ℤ) injects into the complement.
Claim. There exists a continuous embedding $f:S^1\hookrightarrow S^3$ such that the first singular homology of the complement is not the zero object: $H_1(S^3\setminus f(S^1);\mathbb{Z})\not\simeq 0$.
background
PublicSpine is the public dual forcing surface for Recognition Science: δ-stratified claims that papers should cite when they mean "what is forced," parallel to UnifiedForcingChain. Dimension forcing (T8) is not allowed to rest on an arithmetic encoding such as SphereAdmitsCircleLinking (cohomology degree $D-2$ nontrivial). Instead the honest detector is content-typed on Mathlib spaces.
DetectsNontrivialLinking D asserts existence of an embedding $f:S^1\to S^D$ whose complement has nonvanishing first homology. That is the real linking obstruction, stated on singular homology rather than a name-firewall predicate. Upstream, circleH1ZIsoInt_holds gives $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ unconditionally. The unknot-complement retract module supplies the geometric model: the flat unknot $z\mapsto(z,0,0)$ in $S^3$ and a deformation retract of its complement onto the core circle $(0,0,w)$.
Local setting (module doc): the D=3 / eight-tick bridge target is closed by campaign P-d3link; detection is one of the three fields of the content-typed Alexander linking binder.
proof idea
Term-mode inhabitation of the existential. Witness is the flat unknot map from UnknotComplementRetract, packaged with its embedding certificate. Nonvanishing of complement $H_1$ is unknotComplementH1_ne_zero applied to circleH1ZIsoInt_holds: because the complement retracts onto a core circle, $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is a retract of the complement homology, hence the complement cannot be $H_1$-acyclic. No arithmetic encoding and no dimension-forcing lemma is invoked; only real Mathlib singular homology and the retract.
why it matters
This is the detection half (d3_detects) of AlexanderLinkingBridge, the non-encoding purchase binder that replaces the old T8 arithmetic shortcut. Downstream, bridge_of_forces_D3 packages it with the circle $H_1$ isomorphism and a forces_D3 hypothesis into the target D=3 statement; full unconditional inhabitation lives in PublicSpineLinkingClosure.
Framework landmark: T8 ($D=3$ spatial dimensions) in the forcing chain. The module contract forbids citing SphereAdmitsCircleLinking as the architecture claim; papers must go through this geometric detector plus vanishing/forcing at other dimensions (excision spine, arc-complement acyclicity). Campaign P-d3link (2026-07-17/18) closed the detection side with zero sorry on the unknot retract path. Together with eight-tick (CubePeriodEight) this anchors the octave–dimension bridge without encoding cheats.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.