part23_continuous
plain-language theorem explainer
The map extracting the last two coordinates from a point of the unknot complement in S³ is continuous. Anyone assembling the continuous retraction of that complement onto the dual core circle cites this lemma. The proof is a short term-mode composition of the continuous ambient projection with the forgetful maps out of the subtype and ULift wrappers.
Claim. The coordinate map sending a point $y$ of the complement of the standard unknot in $S^3$ to its last two Euclidean coordinates $(y_2,y_3)\in\mathbb{R}^2$ is continuous.
background
This module is a standalone Mathlib-only development of the geometric core behind nontrivial linking detection in dimension 3. It builds the flat unknot $S^1\hookrightarrow S^3$ by $(x_0,x_1)\mapsto(x_0,x_1,0,0)$, records that the map is a topological embedding, introduces the dual core circle valued in the complement, and constructs a continuous retraction of the complement onto that core.
Points of the complement are packaged as a subtype of the universe-lifted three-sphere. The map under study peels those wrappers and applies the linear projection onto the last two coordinates of the ambient Euclidean four-space. Continuity of that ambient projection is already available; the unknot itself is the continuous embedding of the one-sphere along the first two axes.
The local goal is purely topological: enough continuous maps to feed the retraction and, downstream, a singular-homology witness that $H_1$ of the unknot complement is nonzero.
proof idea
Term-mode composition, not a tactic script. Continuity of the ambient two-coordinate projection is composed on the right with the chain of forgetful maps continuous subtype valuation, continuous ULift.down, and continuous subtype valuation again. Each factor is a standard continuous map from Mathlib; no estimates, case splits, or custom continuity arguments appear.
why it matters
Direct input to the continuous retraction of the unknot complement onto the dual core circle. That retraction is defined by normalizing the last two coordinates, and its continuity proof begins by invoking continuity of this coordinate extraction (then inverting the norm on the nonzero locus guaranteed by the complement). The retraction, together with the identity-on-core check, supplies the geometric engine for the nonzero first singular homology of the unknot complement in $S^3$, which is the concrete witness behind DetectsNontrivialLinking 3 in the public spine. In the Recognition forcing chain this is the topological side of the $D=3$ landmark (T8): linking is detected precisely in three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.