D1_no_linking

formal source

 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
 318
 319instance : DecidablePred SupportsNontrivialLinking := fun D =>
 320  if h : D = 3 then isTrue (by rw [h]; exact D3_has_linking)
 321  else isFalse (fun hlink => h (linking_requires_D3 D hlink))
 322
 323/-! ## The Gap-45 Synchronization -/
 324
 325/-- Gap-45 factorization: 45 = 9 × 5 = 3² × 5. -/
 326theorem gap_45_factorization : gap_45 = 9 * 5 := rfl
 327