SphereAdmitsCircleLinking

formal source

 126This replaces the previous tautological definition `D = 3` with a
 127definition grounded in cohomology. The equivalence with D = 3 is now
 128a genuine theorem (`alexander_duality_circle_linking`), not `Iff.rfl`. -/
 129def SphereAdmitsCircleLinking (D : ℕ) : Prop :=
 130  CircleReducedCohomologyNontrivial ((D : ℤ) - 2)
 131
 132/-! ## Theorem: Linking Characterizes D = 3 -/
 133
 134/-- **Alexander Duality Applied to Circle Linking** (Hatcher, Thm 3.44).
 135
 136Non-trivial closed-curve linking in S^D exists iff D = 3.
 137
 138**Proof structure**:
 1391. By definition, `SphereAdmitsCircleLinking D` ↔ H̃^{D-2}(S¹) nontrivial
 1402. By `circle_reduced_cohomology_iff`, this holds iff D - 2 = 1
 1413. For D : ℕ, (D : ℤ) - 2 = 1 iff D = 3
 142
 143This is a genuine theorem requiring the S¹ cohomology axiom, not a
 144definitional identity. -/
 145theorem alexander_duality_circle_linking (D : ℕ) :
 146    SphereAdmitsCircleLinking D ↔ D = 3 := by
 147  unfold SphereAdmitsCircleLinking
 148  rw [circle_reduced_cohomology_iff]
 149  constructor <;> intro h <;> omega
 150
 151/-! ## Derived Facts -/
 152
 153/-- D = 3 admits circle linking (forward direction). -/
 154theorem D3_admits_circle_linking : SphereAdmitsCircleLinking 3 :=
 155  (alexander_duality_circle_linking 3).mpr rfl
 156
 157/-- Circle linking forces D = 3 (reverse direction). -/
 158theorem circle_linking_forces_D3 (D : ℕ) :
 159    SphereAdmitsCircleLinking D → D = 3 :=