Foundation Unknot Complement Retract Retract Core

The retraction that pins the core

A circle drawn in three-dimensional space, tied into the simplest possible knot: the unknot, a loop with no crossing at all. Around that loop lies its complement, the space of all points that are not on the loop itself. The declaration retract_core concerns a second circle, the core, which sits inside that complement, threaded through the middle of the unknot like a ring through a keychain. The statement proves that this core circle can be continuously shrunk back onto itself while staying entirely within the complement, a property called a retraction.

To see what that means, picture the core as a rubber band floating in the space around the unknot. The retraction is a rule that takes any point in the complement and smoothly slides it to a point on the core, without ever touching the unknot itself. The theorem retract_core checks an edge case: when the starting point is already on the core, the rule leaves it exactly where it was. In symbols, the retraction map composed with the inclusion of the core equals the identity map on the core circle. That sounds modest, but it is the precise condition that makes the core a genuine geometric feature of the complement, not an arbitrary choice.

The declaration lives in a machine-checked library of formal theorems, part of the Recognition Science framework's foundation. It is one step in a larger argument that the unknot complement has nontrivial first homology, meaning the space around the unknot contains a hole that cannot be filled in. The retraction is the geometric core of that argument: it provides a way to detect that the complement is not simply a solid blob. The framework uses this to distinguish the unknot from a trivial configuration, though the full linking detection is assembled elsewhere.

What retract_core does not claim is equally important. It does not prove that the unknot is knotted, nor does it establish anything about the original loop's embedding beyond the existence of this retraction. It says nothing about other knots or about the higher-dimensional linking structures the framework ultimately targets. The statement is a local, technical fact: a specific map on a specific space behaves as a retraction should. Its significance comes from what the framework builds on top of it, not from the declaration alone.

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

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

/-- The retraction of the unknot complement onto the core circle. -/
def retractToCore : C(Cpl, TopCat.sphere.{0} 1) where
  toFun := retractFun
  continuous_toFun := by
    apply continuous_uliftUp.comp
    apply Continuous.subtype_mk
    exact ((part23_continuous.norm.inv₀
      fun y => norm_ne_zero_iff.2 (part23_ne_zero y)).smul part23_continuous)

What this page does not claim

The declaration does not prove that the unknot is knotted or that any other knot is nontrivial. It does not establish the full linking detection result, which is assembled elsewhere in the framework. It says nothing about the physical interpretation of recognition events or the cost function.

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: