D1_no_linking
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 in Recognition Science
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.
scope and limits
- Does not establish the linking property for any dimension other than 1.
- Does not reference the eight-tick period or gap-45 synchronization.
- Does not derive the Alexander duality isomorphism.
- Does not connect to the J-cost functional equation or phi-ladder.
- Does not address higher-dimensional unlinking for $D ≥ 4$.
formal statement (Lean)
297theorem D1_no_linking : ¬SupportsNontrivialLinking 1 :=
proof body
Term-mode proof.
298 fun h => absurd (linking_requires_D3 1 h) (by norm_num)
299
300/-- D = 2 does not support linking (Jordan curve theorem — curves separate
301 the plane, linking group H̃^0(S¹) = 0). -/