Foundation Unknot Complement Retract Coord23 Eq Zero Of Mem Range

The coordinate lemma

In four-dimensional space, consider a circle lying flat in the first two coordinate directions: the set of points (x₀, x₁, 0, 0) with x₀² + x₁² = 1. This is the standard unknot, the simplest possible loop. The lemma coord23_eq_zero_of_mem_range states a plain fact about this circle: any point on it has its last two coordinates equal to zero. In symbols, if a point y lies in the range of the unknot map, then y₂ = 0 and y₃ = 0.

This is a coordinate-level observation, but it supports a larger topological claim. The complement of the unknot in the three-sphere S³, the space of points not on the circle, has a nonzero first homology group. That is, the complement is not simply connected; it has a hole in a precise algebraic sense. The lemma coord23_eq_zero_of_mem_range is one of the ingredients that makes this complement well-defined and lets the retraction onto a dual circle work.

In Recognition Science, this lemma is part of a machine-checked library of formal theorems. The framework uses such topological facts to build a bridge between its abstract recognition ledger and the geometry of three-dimensional space. The lemma itself, however, is a purely mathematical statement about coordinates and ranges; it does not by itself assert anything about recognition, cost, or the physical world.

What the lemma does not claim is equally clear. It does not say that every point with zero last two coordinates lies on the unknot; that would be false, since the first two coordinates must also lie on the unit circle. It does not assert anything about the complement's homology; that is a separate theorem. And it makes no statement about the physical significance of the unknot or its complement. The lemma is a narrow, precise tool, and its value lies in what it enables, not in what it alone proves.

/-- Coordinate extraction: a point in the range of the unknot has vanishing
coordinates 2 and 3. -/
lemma coord23_eq_zero_of_mem_range {y : TopCat.sphere.{0} 3}
    (hy : y ∈ Set.range unknot) :
    (ULift.down y).1 2 = 0 ∧ (ULift.down y).1 3 = 0 := by
  obtain ⟨w, hw⟩ := hy
  have h4 : incl01 w.down.1 = (ULift.down y).1 :=
    congrArg (fun v => (ULift.down v).1) hw
  constructor
  · have := congrFun (congrArg WithLp.ofLp h4) 2
    simpa using this.symm
  · have := congrFun (congrArg WithLp.ofLp h4) 3
    simpa using this.symm

What this page does not claim

The lemma does not assert that every point with zero last two coordinates lies on the unknot. The lemma does not by itself establish the nonzero homology of the unknot complement. The lemma makes no statement about the physical or recognition-theoretic significance of the unknot.

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: