Foundation Unknot Complement Retract Unknot Injective

The unknot's embedding

An unknot is the simplest possible knot: a circle that can be deformed into a flat loop without cutting or passing through itself. In the standard mathematical setting, one places such a circle in three-dimensional space, or more precisely on the three-dimensional sphere S³, the one-point compactification of ordinary space. The declaration unknot_injective proves, in the framework's machine-checked library of formal theorems, that the standard map sending a circle to a flat loop in S³ is injective: no two distinct points of the circle land on the same point of the ambient space. This is the basic fact that the flat unknot is a genuine topological embedding, a copy of the circle that does not self-intersect.

The proof works by coordinates. The circle is modeled as the set of unit vectors in a two-dimensional plane, and the unknot is the map that sends a point (x₀, x₁) to the point (x₀, x₁, 0, 0) in four-dimensional Euclidean space, restricted to the unit sphere. The declaration shows that if two points have the same image under this map, then their first two coordinates agree, and since both lie on the unit circle, the points themselves must be equal. The argument is a direct calculation with the coordinate inclusions, and it is fully formalized: the library checks every step against the kernel's rules.

This injectivity is the geometric core of a larger result. The same module constructs a "dual" circle in the complement of the unknot, namely the set of points (0, 0, z₀, z₁) with z₀² + z₁² = 1, and proves that the complement retracts onto this circle: there is a continuous map from the complement to the circle that fixes the circle pointwise. It then shows that the first singular homology of the unknot complement is not zero, given the standard homology of the circle. This nonzero homology is what the framework uses to detect nontrivial linking in its three-dimensional spine construction.

In Recognition Science, this result is a building block. The framework models physical space as a three-dimensional sphere and uses topological invariants of complements of embedded circles to capture linking structure. The injectivity lemma is the first step: it guarantees that the unknot is a proper embedded circle, so that its complement has the expected topological shape. Without this, the later homology computation would not go through.

What the declaration does not claim is equally important. It does not prove that the unknot is the only embedded circle with a nonzero complement homology, nor does it establish any property of knots in general. It does not show that the complement's homology is isomorphic to the integers; it only shows it is not the zero object. And it does not connect this topological fact to any physical measurement or empirical prediction. The declaration is a pure topological lemma, with no claim about the physical world beyond the framework's own modeling choices.

lemma unknot_injective : Function.Injective unknot := by
  intro a b hab
  have h4 : incl01 a.down.1 = incl01 b.down.1 :=
    congrArg (fun w => (ULift.down w).1) hab
  have h2 : a.down.1 = b.down.1 := incl01.injective h4
  exact ULift.ext a b (Subtype.ext h2)

/-- 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 declaration does not prove that the unknot is the only embedded circle with nonzero complement homology. It does not establish any property of knots in general, only of the flat unknot. It does not connect this topological fact to any physical measurement or empirical prediction.

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: