Foundation Alexander Duality D3 Admits Circle Linking

The linking theorem

Two closed curves in ordinary space can pass through each other's rings and hold fast, like links in a chain. This is a familiar fact of everyday geometry, and it turns out to be special to three dimensions. In a plane, two closed curves cannot link at all. In four or more dimensions, there is enough room for any two loops to slip apart without crossing. Only in three dimensions does the structure of space make linking possible.

This fact is a classical result of algebraic topology, the branch of mathematics that studies shapes by assigning them algebraic objects. The precise statement, known as Alexander duality (Hatcher, Algebraic Topology, Theorem 3.44), relates the shape of the space left over after removing a circle from a sphere to the shape of the circle itself. In the framework's machine-checked library of formal theorems, this duality is used to define a predicate that asks whether a D-dimensional sphere admits non-trivial linking of two circles. The definition is not a new assumption; it encodes the standard cohomological computation that the reduced cohomology of a circle is non-zero only in degree one.

The theorem named D3_admits_circle_linking is the forward direction of this characterization: it proves that the three-dimensional sphere does admit circle linking. Its companion, circle_linking_forces_D3, proves the reverse: if a sphere admits circle linking, then the dimension must be three. Together they establish the biconditional that non-trivial circle linking exists if and only if D = 3. The proof is a short argument that unfolds the definition and applies the cohomological characterization, closing with an arithmetic step that reduces D - 2 = 1 to D = 3.

In Recognition Science, this theorem is one step in a chain that aims to show why space has three dimensions. The framework models physical structure from a starting point of recognition events, and this linking result is a topological foundation for that claim. The theorem itself is a formal statement about spheres and circles; it does not, by itself, assert anything about physics. The bridge from this topological fact to the physical claim that space is three-dimensional is a separate question that remains open in the framework. What the theorem does establish, cleanly and without extra axioms, is the mathematical fact that linking is a three-dimensional phenomenon.

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

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

What this page does not claim

This theorem does not prove that physical space is three-dimensional. This theorem does not establish Alexander duality as a formal theorem in the library; that remains open. This theorem does not claim that the definition of circle linking is a physical model of space.

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: