Foundation Unknot Complement Retract Retract Comp Core

The retraction fact

In topology, a circle embedded in three-dimensional space as a simple loop is called an unknot. The space around it, its complement, has a special property: every point in that complement can be continuously moved, or retracted, onto a second circle placed inside the complement. The declaration retract_comp_core proves that this retraction, when applied to points already on that second circle, leaves them fixed. It is a formal statement that the retraction is a genuine one, not a map that accidentally moves the core circle.

The setup uses two circles. The first, the unknot, sits in the plane spanned by the first two coordinates of four-dimensional space, mapped into the unit sphere. The second circle, called the core, lies in the plane spanned by the last two coordinates, and lives entirely in the complement of the unknot. The retraction sends each point of the complement to the core by projecting onto the last two coordinates and then normalizing the result to unit length. The theorem retract_comp_core states that composing this retraction with the inclusion of the core gives the identity map on the core circle. In plain terms, the retraction fixes the core pointwise.

This fact is a geometric core for a larger claim about linking. The same module proves that the first singular homology of the unknot complement is not zero, given that the homology of the circle is the integers. That nonzero homology is what detects that the core circle links the unknot. The retraction fact is a stepping stone: it shows the core is a deformation retract of the complement, which is the standard way to compute the homology of the complement. The declaration itself does not prove the linking claim; it proves the retraction identity that supports it.

In Recognition Science, this retraction fact is part of a library of formal theorems about how linked structures can be detected. The framework models physical structure through a discrete record of events, and linking is one of the topological patterns it uses. The theorem is machine-checked, meaning the proof is verified by a computer program that checks every step. What the declaration does not claim is that the core circle is the only such circle, or that the retraction is unique. It also does not claim that the complement is homeomorphic to the core cross an interval; it claims only the retraction identity.

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

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

The core circle is the only circle with this retraction property. The retraction is unique or canonical in any sense beyond fixing the core. The complement is homeomorphic to the core cross an interval.

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: