linkingNumber

formal source

 106    D=2: always 0 (curves separate)
 107    D=3: non-trivial (Hopf link)
 108    D≥4: always 0 (unlinking possible) -/
 109def linkingNumber (D : ℕ) : ℤ :=
 110  if D = 3 then 1 else 0
 111
 112/-- **HYPOTHESIS**: Irreducible topological linking requires exactly three spatial dimensions.
 113
 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