Foundation Unknot Complement Retract Unknot Complement H1 Ne Zero

The unknot complement's first homology

The statement concerns the complement of an unknot in the three-dimensional sphere. An unknot is a circle embedded in space that is not knotted, the simplest possible loop. Its complement is everything in the sphere except that circle. The declaration unknotComplementH1_ne_zero proves that the first singular homology group of this complement is not the zero object, assuming the standard fact that the first homology of the circle is the integers. In plain terms, the complement has a hole that homology detects; it is not topologically equivalent to a ball.

The proof builds a concrete geometric picture. It defines the unknot as the map taking a point on a circle to the point (x₀, x₁, 0, 0) in four-dimensional coordinates, which is a topological embedding. It then defines a second circle, the core, as the set of points (0, 0, z₀, z₁) that lies entirely in the complement. The key step is a retraction, a continuous map from the complement onto this core circle that leaves every point of the core fixed. The retraction sends a point y in the complement to the normalized vector (y₂, y₃)/‖(y₂, y₃)‖. This construction shows the core circle is a deformation retract of the complement, so the two spaces have the same homology. Since the circle has first homology the integers, the complement's first homology must be nonzero.

The statement is proved in a machine-checked library of formal theorems, using only the standard axioms of the ambient type theory. It is a standalone result about a classical topological space, not a claim about the broader Recognition Science framework. The declaration does not establish that the unknot is nontrivially linked with anything, nor does it prove anything about knotted circles in general. It concerns only the flat unknot in the three-sphere, and its conclusion is that this particular complement is not homologically trivial.

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

theorem retract_comp_core :
    (retractToCore.comp core) = ContinuousMap.id (TopCat.sphere.{0} 1) := by
  ext z
  exact retract_core z

/-- The unknot is a topological embedding (continuous injective map from a
compact space to a Hausdorff space). -/
theorem unknot_isEmbedding : Topology.IsEmbedding unknot :=
  (unknot.continuous.isClosedEmbedding unknot_injective).isEmbedding

What this page does not claim

The declaration does not prove that the unknot is linked with any other circle. It does not establish any property of complements of knotted circles. It does not connect the homology result to the Recognition Science forcing chain.

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: