Pith. sign in
module module moderate

IndisputableMonolith.Foundation.UnknotComplementRetract

show as:
view Lean formalization →

Geometric foundation module that builds the unknot as a continuous embedding of the circle into Euclidean space, together with coordinate inclusions, a projection, and the complement that carries a retract. Anyone reading the public dual forcing spine (δ-stratified tower) cites it for the topological side of the continuum cut. Contents are mostly definitions plus elementary injectivity, continuity, and embedding lemmas.

claimCoordinate inclusions $i_{01}:\mathbb{R}^2\to\mathbb{R}^4$, $(x_0,x_1)\mapsto(x_0,x_1,0,0)$ (linear isometry) and $i_{23}$, continuous projection $p_{23}$, unknot map as a continuous embedding $S^1\hookrightarrow\mathbb{R}^n$, and the open complement $C$ of its image equipped with a retract structure.

background

Recognition Science Foundation work separates a Boolean certificate spine from a public dual surface that is honestly δ-stratified. The continuum cut on that surface needs a concrete geometric model of an embedded circle whose complement retracts in a controlled way; this module supplies that model in Euclidean coordinates.

The basic maps are the linear isometric inclusion of the first two coordinates, the companion inclusion of the last two, and the continuous projection onto the last two. From these one builds an explicit unknot parametrization, proves it is injective and an embedding, and names the open complement of its image. Continuity of the projection is recorded so later arguments can treat the retract as a continuous map on that complement.

Notation follows standard Euclidean product coordinates; no Recognition-specific cost functional appears inside the file itself.

proof idea

Definition-heavy module. Inclusions and the projection are introduced by explicit coordinate formulas; continuity of the projection is a short Mathlib appeal. The unknot map is defined as a concrete parametrization; injectivity and the embedding property are proved by direct coordinate comparison and the closed-map criterion. The complement is the set-theoretic complement of the image, with the retract assembled from the projection and inclusions. No deep algebraic identity or forcing-chain step is proved here.

why it matters in Recognition Science

PublicSpine imports the module as part of the public dual of UnifiedForcingChain. That dual keeps the Boolean spine for pedagogy while exposing a δ-only tower (ℕ/ℤ/ℚ) and an explicit continuum cut (classicalExtension). The unknot complement retract gives a concrete topological carrier for arguments that must not place ¬ℝ under the δ-only regime (panel K2). It does not itself force φ, the eight-tick octave, or D=3; those remain upstream in the T5–T8 chain. The file closes a geometric scaffolding gap so the public spine can cite a named embedding and retract rather than an informal sketch.

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)