part23_ne_zero
plain-language theorem explainer
On the unknot complement in S³, the last two coordinates of any point never vanish. Anyone constructing the continuous retraction onto the dual circle cites this for well-definedness of the normalization step. The proof is pure contradiction: vanishing of those coordinates places the point on the flat unknot, contradicting membership in the complement.
Claim. Let $C$ be the complement in $S^3$ of the flat unknot $(x_0,x_1)\mapsto(x_0,x_1,0,0)$. For every $y\in C$, the coordinate pair $(y_2,y_3)\in\mathbb{R}^2$ is nonzero.
background
The module builds the geometric core of nontrivial linking detection in dimension 3. It realizes the flat unknot as the continuous embedding $S^1\to S^3$ sending $(x_0,x_1)$ to $(x_0,x_1,0,0)$, proves it is a topological embedding, and works throughout with the complement $C$ of its image in $S^3$ (packaged as a TopCat object matching the shape expected by the public linking-homology interface).
Coordinate projections split $\mathbb{R}^4$ into the first two and last two factors. The linear isometry that pads a pair by two zeros is the inclusion used to define the unknot; the dual projection extracts coordinates 2 and 3. Points of $S^3$ are unit vectors in Euclidean 4-space, so the sphere-norm identity $|x|=1$ is available throughout.
The dual circle (the “core”) lives entirely in the last two coordinates and lands in the complement. A continuous retraction of the complement onto that core is obtained by normalizing the last-two-coordinate projection; the present lemma is exactly the statement that the denominator never vanishes on $C$.
proof idea
Argue by contradiction. Write $x\in\mathbb{R}^4$ for the underlying unit vector of $y\in C$, and assume the last-two projection vanishes. Congruence of functions then forces the individual coordinates $x_2=x_3=0$.
The sphere-norm identity $|x|=1$ together with those two zeros collapses to $|(x_0,x_1)|=1$. Packing $(x_0,x_1)$ as a point of $S^1$ and applying the flat inclusion therefore recovers $x$, so $y$ lies in the image of the unknot. That contradicts the defining membership predicate of the complement.
The final identification is by coordinate-wise fin_cases on $\mathrm{Fin},4$, matching the two nonzero head coordinates and the two forced zeros.
why it matters
The lemma is the well-definedness gate for the pointwise retraction $y\mapsto(y_2,y_3)/|(y_2,y_3)|$. That map is packaged as a continuous map from the complement onto the dual circle, and the identity-on-core property then shows the dual circle is a retract of the complement.
Downstream, the retract supplies a nonzero class in first singular homology of the unknot complement (once $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is available), which is the geometric content of DetectsNontrivialLinking 3. The construction is deliberately universe-0 and Mathlib-only so it can be glued later into the public spine linking interface without importing the rest of the monolith.
In the broader Recognition forcing chain this is pure topological scaffolding for the three-dimensional linking step (T8 forces $D=3$); it does not itself touch J-cost, the golden ratio, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.