retractFun
plain-language theorem explainer
Pointwise map sending a point of the unknot complement in S³ to the unit vector formed by its last two coordinates. Anyone building the continuous retraction onto the dual core circle cites this. The body normalizes part23 after the complement lemma that those coordinates cannot vanish.
Claim. For each point $y$ in the complement of the flat unknot in $S^3$, return the point of $S^1$ given by normalizing the last two Euclidean coordinates: $(y_2,y_3)/\|(y_2,y_3)\|$.
background
The module constructs the standard flat unknot $S^1\hookrightarrow S^3$ by $(x_0,x_1)\mapsto(x_0,x_1,0,0)$, proves it is a topological embedding, and works entirely in universe 0 with Mathlib spheres. The complement object Cpl is the TopCat subtype of $S^3$ excluding the image of that unknot; it is the exact shape expected by the public linking-complement homology interface.
On that complement one extracts the last two coordinates via part23. The key well-definedness fact is part23_ne_zero: if those coordinates vanished the point would lie on the unknot, contradicting membership in the complement. The dual core circle embeds the opposite way, $(z_0,z_1)\mapsto(0,0,z_0,z_1)$, landing inside the complement. The present map is the set-theoretic retraction of the complement onto that core circle.
proof idea
Pure definitional construction, not a tactic proof. Extract part23 y in $\mathbb{R}^2$, scale by the reciprocal of its Euclidean norm, and pack the result as a point of the Mathlib sphere $S^1$ (via ULift.up and a subtype). The membership obligation ‖v‖=1 is discharged by rewriting with mem_sphere_zero_iff_norm, norm_smul, norm_inv, and norm_norm, then cancelling with inv_mul_cancel₀ using part23_ne_zero y.
why it matters
This is the underlying point map for retractToCore, the continuous retraction of the unknot complement onto the dual core circle. That retraction, together with the identity-on-core lemma, supplies the geometric engine for unknotComplementH1_ne_zero: the first singular homology of the complement is nontrivial once $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is known. The whole chain is the standalone geometric core of DetectsNontrivialLinking 3 and is shaped to glue into PublicSpine.linkingComplementH1 elsewhere. In the Recognition foundation it witnesses that the unknot in $S^3$ is detected by complement homology, a topological prerequisite for linking-sensitive recognition arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.