forces_D3
plain-language theorem explainer
Nontrivial circle linking detection on the sphere forces spatial dimension exactly 3. Anyone citing Recognition Science T8, or inhabiting the Alexander linking bridge on the public spine, needs this unconditional statement. The proof is a short term application of the arc-acyclic forcing lemma, supplying H₁-acyclicity of every arc complement in every dimension.
Claim. For every natural number $D$, if there exists a continuous embedding $f \colon S^1 \hookrightarrow S^D$ such that the first homology of the complement is nontrivial, then $D = 3$.
background
The public-spine predicate "detects nontrivial linking in dimension $D$" means: there is a topological embedding of the circle into the $D$-sphere whose complement has nonvanishing first homology (with integer coefficients). That is the content-typed stand-in for classical circle linking, without arithmetic encodings of cohomology.
Low dimensions $0$ and $1$ already rule out linking by elementary position (curves cannot be disjoint and linked). High dimensions ($2$ and $\ge 4$) are handled by a Mayer–Vietoris reduction that reduces circle-complement nonvanishing to a statement about arc complements. The key geometric input is arc-complement acyclicity (Hatcher 2B.1, arc case): every embedded interval in $S^D$ has $H_1$-acyclic complement, in every $D$.
This module closes the public-spine linking campaign by assembling those vanishing results into an unconditional forcing statement, bypassing the older axiomatic linking_requires_D3 on the spine.
proof idea
One-line term proof. Apply the assembly lemma forces_D3_of_arcAcyclic, which already packages the low-dimensional vanishing cases with the high-dimensional Mayer–Vietoris reduction. The only remaining hypothesis is arc-complement $H_1$-acyclicity in every dimension; supply it by the constant family of the proved theorem arcComplementsAcyclic. No extra case split appears at this layer.
why it matters
This is the unconditional half of T8 on the public spine: nontrivial linking detection forces $D=3$. It is the forces_D3 field of AlexanderLinkingBridge, so D3_of_bridge is just projection of that field. Downstream, T8_Via_Realization_Bridge in the unified forcing chain cites it, and the Mathlib cohomology bridge structures treat it as the dimension-forcing half of the circle-linking backend.
Together with the already-proved detection half (the flat unknot in $S^3$ has nonvanishing complement $H_1$), the bridge is fully inhabited: some dimension detects linking, and only dimension 3 can. That closes campaign P-d3link without residual axioms on the public spine, and pins the RS landmark that spatial dimension is forced by Alexander duality rather than by the eight-tick or gap-45 arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.