Foundation Alexander Duality Circle Linking Forces D3

Circle linking and dimension

In topology, two circles embedded in a sphere can be linked like chain links, or they can be separated. The classical fact, known from Alexander duality (Hatcher, Algebraic Topology, Theorem 3.44), is that such non-trivial linking exists only in a 3-dimensional sphere. In 1 or 2 dimensions there is no room to link, and in 4 or more dimensions there is enough room to untie any pair. This is a standard result with a standard proof: the first homology of the complement of a circle in the D-sphere is isomorphic to the reduced cohomology of the circle in degree D-2, and that group is non-zero only when D-2 equals 1, so D equals 3.

The Recognition Science framework's machine-checked library of formal theorems formalizes this argument. Its declaration circle_linking_forces_D3 states that if a D-sphere admits non-trivial linking of disjoint embedded circles, then D must equal 3. The proof is not a new mathematical discovery; it is a formal verification of the classical topological argument. The library defines the linking predicate not as a bare assertion that D equals 3, but through the cohomological condition: the reduced cohomology of the circle in degree D-2 is non-trivial. The theorem then derives D equals 3 from that condition.

This formalization replaces an earlier version that simply declared the equivalence as an axiom. Now the predicate has a concrete definition, and the theorem is proved from it. The library also proves the converse: in dimension 3, circle linking exists, and in dimensions 2 or lower, and 4 or higher, it does not. These are all theorems in the library, checked by the kernel.

What the declaration does not claim is just as important. It does not prove Alexander duality itself; that remains an open target in the library. The definition of the linking predicate encodes the cohomological computation of the circle, but the full duality theorem is not yet formalized. The declaration also does not make any physical claim about space being three-dimensional. It is a topological theorem about spheres and embedded circles, not a statement about the physical universe. The bridge from this topological fact to physical space is a separate question, and it remains open.

/-- **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

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

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

/-- 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

It does not prove Alexander duality itself; that remains an open target. It makes no physical claim about the dimensionality of space. The bridge from topology to physical space is not established by this declaration.

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: