linking_dimension_odd

formal source

  66
  67theorem circle_links_in_three : linking_dimension 1 = 3 := by norm_num
  68
  69theorem linking_dimension_odd (p : ℕ) : Odd (linking_dimension p) := by
  70  use p; unfold linking_dimension; omega
  71
  72/-! ## D = 3 Forcing from Linking
  73
  74The physical argument: recognition events require distinguishable
  75topological linking (knots/links). The simplest non-trivial link
  76is between circles. Circles link non-trivially only in D = 3. -/
  77
  78structure LinkingForcesD3 where
  79  smallest_linker : ℕ := 1  -- S^1 (circle)
  80  linking_requires : linking_dimension 1 = 3
  81  no_linking_in_2D : ∀ D, D ≤ 2 → ¬(∃ p, linking_dimension p = D ∧ p ≥ 1)
  82  linking_in_3D : linking_dimension 1 = 3
  83
  84theorem linking_forces_d3_cert : LinkingForcesD3 where
  85  linking_requires := circle_links_in_three
  86  no_linking_in_2D := by
  87    intro D hD ⟨p, hp, hp1⟩
  88    unfold linking_dimension at hp
  89    omega
  90  linking_in_3D := circle_links_in_three
  91
  92/-! ## Certificate -/
  93
  94structure AlexanderDualityCert where
  95  circle_degree : circle_cohomology.reduced_cohomology_rank 1 = 1
  96  circle_only_degree : ∀ k, k ≠ 1 → circle_cohomology.reduced_cohomology_rank k = 0
  97  d3_from_linking : linking_dimension 1 = 3
  98
  99theorem alexander_duality_cert_exists : Nonempty AlexanderDualityCert :=