H_LinkingDimensionUniqueness

formal source

 114    STATUS: SCAFFOLD — Connects linking invariants to dimensions.
 115    TODO: Prove that linking number is only invariant in D=3 for 1-spheres.
 116    FALSIFIER: Discovery of a non-trivial linking invariant for 1-spheres in D ≠ 3. -/
 117def H_LinkingDimensionUniqueness : Prop :=
 118  ∀ D : ℕ, D ≥ 2 → (linkingNumber D ≠ 0 ↔ D = 3)
 119
 120/-- D=3 is the unique dimension with irreducible linking. -/
 121theorem Q3_unique_linking_dimension :
 122    ∀ D : ℕ, D ≥ 2 → (linkingNumber D ≠ 0 ↔ D = 3) := by
 123  intro D hD
 124  constructor
 125  · intro hLink
 126    unfold linkingNumber at hLink
 127    split_ifs at hLink with h
 128    · exact h
 129    · simp at hLink
 130  · intro hD3
 131    unfold linkingNumber
 132    simp [hD3]
 133
 134/-- The cube Q₃ is the unique linking-compatible polytope.
 135    (Reformulated: Linking structure implies D=3) -/
 136theorem cube_uniqueness :
 137    ∀ D : ℕ, (linkingNumber D ≠ 0) ↔ D = 3 := by
 138  intro D
 139  constructor
 140  · intro h
 141    unfold linkingNumber at h
 142    split_ifs at h with hD
 143    · exact hD
 144    · contradiction
 145  · intro h
 146    rw [h]
 147    unfold linkingNumber