Foundation Alexander Duality Alexander Duality Circle Linking

Circle linking and three dimensions

Circle linking is a topological phenomenon: two closed loops that cannot be separated without cutting. In a plane, no two loops link. In ordinary three-dimensional space, they can, as with the Hopf link, where each circle passes through the other's hole. In four or more dimensions, there is enough room to untangle any pair of loops. The classical fact, known from algebraic topology, is that non-trivial linking of circles in a sphere exists only in dimension three.

The framework's machine-checked library of formal theorems encodes this fact as a theorem named alexander_duality_circle_linking. The theorem states that a sphere of dimension D admits non-trivial circle linking if and only if D equals 3. The proof uses Alexander duality, a standard result (Hatcher, Algebraic Topology, Theorem 3.44) relating the homology of a complement to the cohomology of the subspace. For a circle embedded in a D-sphere, the relevant reduced cohomology group of the circle is non-zero only in degree 1, which forces D minus 2 to equal 1, hence D equals 3.

In Recognition Science, this theorem is a bridge predicate. Earlier versions of the framework defined the linking property directly as "D equals 3". The new declaration replaces that definitional tautology with a predicate grounded in the reduced cohomology of the circle, and proves the equivalence with D equals 3 as a genuine theorem. The framework's library also derives the two directions separately: dimension three admits circle linking, and circle linking forces dimension three. It further proves that no circle linking exists in dimensions at most two or at least four.

What the declaration does not claim is as important as what it proves. The theorem does not prove Alexander duality itself; that remains an open target in the library. The predicate encoding the circle's reduced cohomology is a named identification of a standard computation, not a proof from more basic cohomology theory. The theorem does not assert that physical space is three-dimensional because of this topological fact. That physical claim would require a separate bridge from recognition events to spatial linking, which the framework marks as 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

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

Alexander duality itself is not proved in the library. The theorem does not assert that physical space is three-dimensional because of this topological fact. The reduced cohomology of the circle is encoded as a named identification, not derived from a full cohomology theory.

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: