linking_requires_D3
plain-language theorem explainer
If a spatial dimension D supports nontrivial linking of closed curves then D equals 3. Researchers deriving spatial dimension from topological conservation in ledger models cite this to exclude other dimensions. The proof is a one-line wrapper applying the forward direction of the Alexander duality equivalence for circle linking.
Claim. Let $D$ be a spatial dimension. If $D$ supports nontrivial linking of disjoint closed curves (i.e., the reduced cohomology satisfies $H̃_1(S^D ∖ S¹) ≅ ℤ$), then $D = 3$.
background
The Dimension Forcing module proves that spatial dimension equals 3 is forced by the RS framework through four arguments, of which the linking argument is the first. Dimension is an abbreviation for ℕ. SupportsNontrivialLinking D is defined as SphereAdmitsCircleLinking D, the predicate that S^D admits disjoint S¹-embeddings with nonzero linking number; the module doc states this holds precisely when the reduced cohomology H̃₁(S^D ∖ S¹) is isomorphic to ℤ, which occurs only for D = 3.
proof idea
The proof is a one-line wrapper that applies the forward (mp) direction of alexander_duality_circle_linking D. Because SupportsNontrivialLinking D unfolds directly to SphereAdmitsCircleLinking D, the equivalence proved upstream immediately yields D = 3.
why it matters
This is the primary theorem for the topological linking argument in the Dimension Forcing module and implements the T8 claim that D = 3. It feeds dimension_unique, D1_no_linking, D2_no_linking, D4_no_linking and high_D_no_linking. The result draws on Alexander duality (quoted upstream as “Non-trivial closed-curve linking in S^D exists iff D = 3”) without invoking the eight-tick period or gap-45 synchronization also present in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 3 of 3)
-
P-wave magnets show parity-breaking Fermi surfaces
"We demonstrate a strong parity-breaking and anisotropic symmetry lowering of spin-polarized and time-reversal symmetric Fermi surfaces in a representative p-wave magnet CeNiAsO."
-
One model reconstructs metric 3D scenes from images and inputs
"MapAnything leverages a factored representation of multi-view scene geometry, i.e., a collection of depth maps, local ray maps, camera poses, and a metric scale factor that effectively upgrades local reconstructions into a globally consistent metric frame."
-
Sparse attention scales transformers to 100,000-step sequences
"We introduce sparse factorizations of the attention matrix which reduce this to O(n√n)... We call networks with these changes Sparse Transformers, and show they can model sequences tens of thousands of timesteps long using hundreds of layers... setting a new state of the art for density modeling of Enwik8, CIFAR-10, and ImageNet-64."