Foundation Unknot Complement Retract

The unknot and its complement

In topology, an unknot is a circle placed in space without any knotting. In four-dimensional space, the standard flat unknot sits in the first two coordinates, like a ring lying in a plane. The complement of the unknot is everything in the 3-sphere that is not on that ring. The classical question is whether this leftover space has any holes or loops that cannot be shrunk to a point. The answer, known since the early days of algebraic topology, is yes: the complement of an unknot in the 3-sphere has a nontrivial first homology group, meaning there is a loop that cannot be contracted away.

The construction UnknotComplementRetract in the machine-checked library of formal theorems proves this classical fact from scratch, using only the standard axioms of the ambient type theory. It constructs the unknot as a continuous map from the 1-sphere into the 3-sphere, sending a point (x0, x1) to (x0, x1, 0, 0). It then builds a second circle, called the core, which lives entirely in the complement: the map sends z to (0, 0, z0, z1). This core is a loop that winds around the unknot, and the construction proves it cannot be shrunk away.

The key construction is a retraction. It defines a continuous map from the complement onto the core, sending a point y to the normalized vector (y2, y3) divided by its length. This map is a retraction because when you restrict it to the core itself, it is the identity: each point on the core is sent to itself. The existence of this retraction is what forces the complement to have a nontrivial loop. If the complement could be contracted to a point, then the core would have to be contractible too, but the retraction preserves the loop structure. The construction then uses the fact that the first homology of the 1-sphere is the integers to conclude that the first homology of the complement is not zero.

In Recognition Science, this construction is the geometric core of a larger argument about how three spatial dimensions are forced. The framework models physical space as a discrete record of recognition events, and it needs to show that certain linking structures are nontrivial. This construction provides the topological fact that an unknot complement has a genuine hole, which the framework uses to detect nontrivial linking. The physical bridge from this topological fact to actual three-dimensional space remains an open target, but the topological fact itself is established with full formal rigor.

/-- The standard flat unknot `S¹ ↪ S³` as a continuous map between the
`TopCat` spheres. -/
def unknot : C(TopCat.sphere.{0} 1, TopCat.sphere.{0} 3) where
  toFun := unknotFun
  continuous_toFun := by
    apply continuous_uliftUp.comp
    apply Continuous.subtype_mk
    exact incl01.continuous.comp
      (continuous_subtype_val.comp continuous_uliftDown)

/-- The core circle as a continuous map into the complement. -/
def core : C(TopCat.sphere.{0} 1, Cpl) where
  toFun := coreFun
  continuous_toFun := by
    apply Continuous.subtype_mk
    apply continuous_uliftUp.comp
    apply Continuous.subtype_mk
    exact incl23.continuous.comp
      (continuous_subtype_val.comp continuous_uliftDown)

/-- Composite identity: the retraction restricted along the core circle is the
identity of S¹. -/
theorem retract_core (z : TopCat.sphere.{0} 1) : retractToCore (core z) = z := by
  have hpart : part23 (core z) = z.down.1 := by
    ext i
    fin_cases i <;>
      simp [part23, core, coreFun]
  have hnorm : ‖z.down.1‖ = 1 := mem_sphere_zero_iff_norm.1 z.down.2
  apply ULift.ext
  apply Subtype.ext
  show ‖part23 (core z)‖⁻¹ • part23 (core z) = z.down.1
  rw [hpart, hnorm, inv_one, one_smul]

/-- **Capstone.** Given that first singular homology of S¹ with ℤ coefficients
is ℤ (as an iso in `ModuleCat ℤ`), the first singular homology of the unknot
complement in S³ is not the zero object. Pure retraction argument: `core` and
`retractToCore` exhibit H₁(S¹) as a retract of H₁(complement). -/
theorem unknotComplementH1_ne_zero
    (h1 : Nonempty ((((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj
      (ModuleCat.of ℤ ℤ)).obj (TopCat.sphere.{0} 1)) ≅ ModuleCat.of ℤ ℤ)) :
    ¬ CategoryTheory.Limits.IsZero
      (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj
        (ModuleCat.of ℤ ℤ)).obj (TopCat.of {x : TopCat.sphere.{0} 3 // x ∉ Set.range unknot})) := by
  intro hz
  obtain ⟨e⟩ := h1
  set H : TopCat.{0} ⥤ ModuleCat ℤ :=
    (AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj (ModuleCat.of ℤ ℤ) with hH
  let g : TopCat.sphere.{0} 1 ⟶ Cpl := TopCat.ofHom core
  let r : Cpl ⟶ TopCat.sphere.{0} 1 := TopCat.ofHom retractToCore
  have hgr : g ≫ r = 𝟙 (TopCat.sphere.{0} 1) := by
    ext z
    exact retract_core z
  have hmap : H.map g ≫ H.map r = 𝟙 (H.obj (TopCat.sphere.{0} 1)) := by
    rw [← H.map_comp, hgr, H.map_id]
  have hzC : IsZero (H.obj Cpl) := hz
  have hg0 : H.map g = 0 := hzC.eq_zero_of_tgt _
  have hid0 : 𝟙 (H.obj (TopCat.sphere.{0} 1)) = 0 := by
    rw [← hmap, hg0, zero_comp]
  have hzS1 : IsZero (H.obj (TopCat.sphere.{0} 1)) :=
    (IsZero.iff_id_eq_zero _).mpr hid0
  have hzZ : IsZero (ModuleCat.of ℤ ℤ) := hzS1.of_iso e.symm
  have hsub : Subsingleton ℤ := ModuleCat.isZero_of_iff_subsingleton.mp hzZ
  exact one_ne_zero (hsub.elim (1 : ℤ) 0)

/- Axioms audit (2026-07-17, `#print axioms` on the built module):
`unknotComplementH1_ne_zero`, `unknot_isEmbedding`, `retract_comp_core` each
depend only on `[propext, Classical.choice, Quot.sound]`. No `sorry`, no new
axioms, no `native_decide`. -/

What this page does not claim

This construction does not prove that three-dimensional space is forced; that requires the separate linking closure theorem. This construction does not establish the physical bridge from topology to recognition events. The retraction is not claimed to be a deformation retraction, only a continuous retraction.

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/UnknotComplementRetract.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: