D3_has_linking

formal source

 284
 285/-- D = 3 supports non-trivial linking (Hopf link witnesses nonzero element
 286    of the linking group H̃₁(S³ \ S¹) ≅ ℤ). -/
 287theorem D3_has_linking : SupportsNontrivialLinking 3 :=
 288  (alexander_duality_circle_linking 3).mpr rfl
 289
 290/-- **T8 PRIMARY THEOREM**: Linking requires D = 3.
 291    Proof: Alexander duality — no reference to 8-tick or gap-45. -/
 292theorem linking_requires_D3 (D : Dimension) :
 293    SupportsNontrivialLinking D → D = 3 :=
 294  (alexander_duality_circle_linking D).mp
 295
 296/-- D = 1 does not support linking (collinear — curves cannot be disjoint). -/
 297theorem D1_no_linking : ¬SupportsNontrivialLinking 1 :=
 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). -/
 302theorem D2_no_linking : ¬SupportsNontrivialLinking 2 :=
 303  fun h => absurd (linking_requires_D3 2 h) (by norm_num)
 304
 305/-- D = 4 does not support linking (codimension ≥ 2 — curves unlink by
 306    general position, linking group H̃^2(S¹) = 0). -/
 307theorem D4_no_linking : ¬SupportsNontrivialLinking 4 :=
 308  fun h => absurd (linking_requires_D3 4 h) (by norm_num)
 309
 310/-- D ≥ 4 does not support linking (Alexander duality: linking group trivial
 311    for D ≥ 4 since H̃^{D-2}(S¹) = 0 when D-2 ≥ 2). -/
 312theorem high_D_no_linking (D : Dimension) (hD : D ≥ 4) :
 313    ¬SupportsNontrivialLinking D := by
 314  intro h
 315  have heq := linking_requires_D3 D h
 316  subst heq
 317  norm_num at hD