part23
plain-language theorem explainer
Extracts the last two Euclidean coordinates of a point in the unknot complement in S³, landing in R². Used by anyone building the radial retraction onto the dual circle (y₂,y₃)/‖(y₂,y₃)‖. The body is a one-line composition of the linear projection with the subtype and ULift unwraps that present a complement point.
Claim. For a point $y$ in the complement of the flat unknot in $S^3$, write $\mathrm{part}_{23}(y)$ for the pair of coordinates $(y_2,y_3)\in\mathbb{R}^2$ obtained by projecting the underlying vector in $\mathbb{R}^4$ onto the last two axes.
background
The module builds a geometric core for nontrivial linking detection in dimension 3: the flat unknot $S^1\hookrightarrow S^3$, $(x_0,x_1)\mapsto(x_0,x_1,0,0)$, its complement as a TopCat object, a dual core circle in the last two coordinates, and a continuous retraction of the complement onto that circle.
A point of the complement is a point of $S^3\subset\mathbb{R}^4$ that is not in the image of the unknot, so at least one of coordinates 2 or 3 is nonzero. The linear map $\mathrm{proj}_{23}:\mathbb{R}^4\to\mathbb{R}^2$, $y\mapsto(y_2,y_3)$, is the coordinate projection used throughout; continuity follows from finite dimension. The present definition simply applies that projection after unwrapping the subtype and universe-lift packaging of a complement point.
proof idea
Definitional one-liner: unwrap the complement point to its underlying vector in Euclidean 4-space (subtype value, then ULift.down), then apply the linear projection onto coordinates 2 and 3. No separate proof obligations; well-definedness and continuity are recorded in sibling lemmas.
why it matters
This coordinate slice is the algebraic heart of the retraction. The point-level retraction sends $y$ to the unit vector $(y_2,y_3)/|(y_2,y_3)|$, which is only defined once one knows the slice is nonzero on the complement; that nonvanishing and the continuity of the slice feed the continuous retraction onto the core circle. The identity of the retraction along the core circle is proved by observing that the slice of a core point is the core point itself (unit norm). Together these facts give a retract of the unknot complement onto $S^1$, hence nontrivial $H_1$, matching the geometric input expected by the public linking-complement homology interface for DetectsNontrivialLinking 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.