D4_no_linking

formal source

 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
 328/-- Gap-45 has factor 9 = 3². -/
 329theorem gap_45_has_factor_9 : 9 ∣ gap_45 := ⟨5, rfl⟩
 330
 331/-- The sync period 360 = 8 × 45 / gcd(8,45) = 360. -/
 332theorem sync_factorization : sync_period = 8 * 45 := by
 333  unfold sync_period eight_tick gap_45
 334  -- lcm(8, 45) = 8 * 45 / gcd(8, 45) = 360 / 1 = 360
 335  -- But actually gcd(8, 45) = 1, so lcm = 8 * 45 = 360
 336  rfl
 337