Pith. sign in
module module moderate

IndisputableMonolith.Foundation.UnknotComplementRetract

show as:
view Lean formalization →

Foundation module assembling the unknot as an embedded circle in Euclidean space, together with coordinate inclusions, a continuous projection, and the open complement. Topologists and RS foundation readers cite it when a concrete retract of the unknot complement is needed. The file is mostly definitions and short Mathlib embedding lemmas, not a long forcing argument.

claimCoordinate inclusions $i_{01}\colon\mathbb{R}^2\to\mathbb{R}^4$, $(x_0,x_1)\mapsto(x_0,x_1,0,0)$ and $i_{23}$, a continuous projection $p_{23}$, an embedded unknot $u\colon S^1\hookrightarrow\mathbb{R}^n$, and its open complement $C=\mathbb{R}^n\setminus u(S^1)$, set up so that a retract of $C$ can be stated.

background

The module lives in the Foundation layer of Recognition Science and imports only Mathlib. It supplies the elementary Euclidean geometry behind an unknot complement retract: linear isometries that pad $\mathbb{R}^2$ into $\mathbb{R}^4$ by zeros in the last (resp. first) two coordinates, the matching projection onto the last two coordinates, and pointwise coordinate lemmas for those maps.

The unknot is packaged as a function unknotFun promoted to an embedding (unknot_isEmbedding), with injectivity recorded separately. The open set $C$ is the complement of the image. These are standard differential-topology ingredients; the RS interest is that a retract of the complement can later feed $\delta$-stratified forcing surfaces rather than a Boolean certificate spine.

proof idea

Definition-heavy module. Inclusions and the projection are introduced as explicit maps; continuity of the projection and the embedding property of the unknot are short Mathlib-facing lemmas (injectivity, then IsEmbedding). No multi-step forcing chain is proved here; the file stops once the complement and the embedding data exist.

why it matters in Recognition Science

Imported by Foundation.PublicSpine, the public dual of UnifiedForcingChain. PublicSpine keeps the Boolean spine for pedagogy and exposes a $\delta$-stratified map (forced_tower_holds, continuum cut via classicalExtension). An unknot-complement retract is a concrete topological witness that can sit under that dual surface without replacing UFC. It does not itself force $\phi$, the eight-tick octave, or $D=3$; those remain T6–T8 landmarks upstream in the forcing chain.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (23)