Foundation Alexander Duality Sphere Admits Circle Linking

Circle linking in three dimensions

In three-dimensional space, two closed loops can be linked together like the rings of a chain. In a plane, or in a space of four or more dimensions, such linking is impossible. This is a classical fact of topology, the branch of mathematics that studies properties preserved under continuous deformation. The standard proof uses Alexander duality, a theorem named after the American topologist James W. Alexander, published in 1922. It relates the holes in a space to the holes in its complement.

The framework's library, a machine-checked collection of formal theorems, encodes this result. Its declaration SphereAdmitsCircleLinking, a formal statement about a sphere of a given dimension, asserts that the D-dimensional sphere admits non-trivial linking of two disjoint embedded circles. The declaration is not a new axiom; it is a definition grounded in the cohomology of the circle, a standard algebraic invariant. The library proves, as a theorem, that this linking exists if and only if D equals 3. It also proves the two directions separately: dimension three admits linking, and any dimension that admits linking must be three.

The proof proceeds by computing the relevant cohomology group. For a circle embedded in a D-dimensional sphere, Alexander duality identifies the first homology of the complement with the reduced cohomology of the circle in degree D minus 2. The reduced cohomology of a circle is non-zero only in degree 1. Therefore the linking group is non-trivial exactly when D minus 2 equals 1, which is to say D equals 3. For dimensions two or less, and for dimensions four or more, the relevant cohomology group vanishes, so no linking occurs.

This formal result is a topological theorem, not a physical one. It does not by itself establish that physical space is three-dimensional. The framework's broader project aims to derive the three dimensions of space from its theory of recognition, and this circle-linking theorem is one piece of that larger argument. But the step from this topological fact to the physical claim remains open. The declaration also does not claim to have formalized Alexander duality itself; it uses the duality as a named identification, not as a proved theorem within the library.

/-- **Alexander Duality Applied to Circle Linking** (Hatcher, Thm 3.44).

Non-trivial closed-curve linking in S^D exists iff D = 3.

**Proof structure**:
1. By definition, `SphereAdmitsCircleLinking D` ↔ H̃^{D-2}(S¹) nontrivial
2. By `circle_reduced_cohomology_iff`, this holds iff D - 2 = 1
3. For D : ℕ, (D : ℤ) - 2 = 1 iff D = 3

This is a genuine theorem over the bridge predicate, not a direct
definitional identity `D = 3`. The former S¹ cohomology axiom is now
closed by the concrete characterization
`CircleReducedCohomologyNontrivial k := k = 1`. -/
theorem alexander_duality_circle_linking (D : ℕ) :
    SphereAdmitsCircleLinking D ↔ D = 3 := by
  unfold SphereAdmitsCircleLinking
  rw [circle_reduced_cohomology_iff]
  constructor <;> intro h <;> omega

/-- D = 3 admits circle linking (forward direction). -/
theorem D3_admits_circle_linking : SphereAdmitsCircleLinking 3 :=
  (alexander_duality_circle_linking 3).mpr rfl

/-- Circle linking forces D = 3 (reverse direction). -/
theorem circle_linking_forces_D3 (D : ℕ) :
    SphereAdmitsCircleLinking D → D = 3 :=
  (alexander_duality_circle_linking D).mp

/-- No circle linking in D ≤ 2.
Proof: H̃^{D-2}(S¹) = 0 for D - 2 ≤ 0, since S¹ has no nontrivial
reduced cohomology in non-positive degrees. -/
theorem no_circle_linking_low_dim (D : ℕ) (hD : D ≤ 2) :
    ¬SphereAdmitsCircleLinking D := by
  intro h
  have := circle_linking_forces_D3 D h
  omega

/-- No circle linking in D ≥ 4.
Proof: H̃^{D-2}(S¹) = 0 for D - 2 ≥ 2, since S¹ has no nontrivial
reduced cohomology above degree 1. -/
theorem no_circle_linking_high_dim (D : ℕ) (hD : D ≥ 4) :
    ¬SphereAdmitsCircleLinking D := by
  intro h
  have := circle_linking_forces_D3 D h
  omega

What this page does not claim

The declaration does not prove Alexander duality itself; it uses the duality as a named identification. The declaration does not establish that physical space is three-dimensional; that step remains open. The declaration does not claim to have formalized the cohomology of the circle against a standard library; it encodes the computation as a concrete definition.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/AlexanderDuality.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: