D1_no_linking
plain-language theorem explainer
Dimension 1 admits no non-trivial linking of closed curves. Researchers deriving the necessity of three spatial dimensions in the Recognition Science framework cite this case when excluding collinear configurations from the topological veto. The proof is a one-line term that applies the general implication linking requires D equals 3 and obtains an immediate numerical contradiction.
Claim. $¬$SupportsNontrivialLinking$(1)$, where SupportsNontrivialLinking$(D)$ asserts that $S^D$ admits disjoint embeddings of $S^1$ with nonzero linking number (equivalent to $D=3$ by Alexander duality).
background
The DimensionForcing module proves that spatial dimension equals 3 via four arguments, beginning with the topological linking argument. SupportsNontrivialLinking$(D)$ is defined as SphereAdmitsCircleLinking$(D)$, which by Alexander duality holds precisely when the reduced homology group $H̃_1(S^D ∖ S^1)$ is isomorphic to $ℤ$, i.e., only for $D=3$. The upstream theorem linking_requires_D3 states that SupportsNontrivialLinking$(D)$ implies $D=3$, with a parallel statement in TopologicalVeto.
proof idea
The proof is a one-line term-mode wrapper. It assumes SupportsNontrivialLinking 1, applies the upstream lemma linking_requires_D3 to conclude that the dimension equals 3, and obtains a contradiction with the numeral 1 via norm_num.
why it matters
This theorem closes the $D=1$ case in the linking argument of the DimensionForcing module. It supports the primary claim that linking requires $D=3$ and contributes to the framework landmark T8 forcing three spatial dimensions. The module documentation states that only $D=3$ supports stable topological conservation via non-trivial links, while $D=1$ has no room for linking as everything is collinear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.