retractToCore
plain-language theorem explainer
Continuous retraction from the unknot complement in S³ onto the dual core circle S¹, sending each point to the normalization of its last two coordinates. Anyone proving nontrivial H₁ of the complement via a retract argument cites this map. Continuity is built from continuous projection of those coordinates, nonzero-norm inversion, and scalar multiplication.
Claim. There is a continuous map $r: S^3\setminus U\to S^1$ given by $r(y)=(y_2,y_3)/\|(y_2,y_3)\|$, where $U\subset S^3$ is the flat unknot $\{(x_0,x_1,0,0)\}$ and the codomain is the unit circle in the last two coordinates.
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 $U:S^1\hookrightarrow S^3$, $(x_0,x_1)\mapsto(x_0,x_1,0,0)$, proves it is a topological embedding, and forms the complement as a TopCat object $Cpl={x\in S^3:x\notin\mathrm{range}(U)}$.
The dual core circle sits in the complementary plane: $z\mapsto(0,0,z_0,z_1)$, valued in $Cpl$. The last-two-coordinate projection on the complement never vanishes (points of $U$ are exactly those with vanishing last two coordinates), so normalizing that $\mathbb{R}^2$-valued projection yields a well-defined map to $S^1$. The present declaration packages that map as a continuous map of topological spaces $Cpl\to S^1$.
Upstream, core supplies the continuous inclusion of $S^1$ into $Cpl$ against which the retraction identity will be checked; part23_continuous is the continuous extraction of coordinates 2 and 3 used in the continuity argument.
proof idea
Definitional packaging: the underlying function is retractFun (normalize the last two coordinates). Continuity is proved by composing continuous ulift with a subtype constructor, then writing the normalized vector as scalar multiplication of the continuous projection part23 by the reciprocal of its Euclidean norm. The reciprocal is continuous on the complement because part23_ne_zero guarantees the norm never vanishes there (norm_ne_zero_iff).
why it matters
This is item 4 in the module's geometric checklist and the map that makes the unknot complement a retract of $S^1$ in the opposite direction from core. Downstream, retract_core proves $r\circ\mathrm{core}=\mathrm{id}_{S^1}$, and retract_comp_core lifts that to an equality of continuous maps. The capstone unknotComplementH1_ne_zero then runs a pure retraction argument: singular homology $H_1(-;\mathbb{Z})$ sends the retract pair to a retract of modules, so $H_1(S^1)\cong\mathbb{Z}$ embeds into $H_1(Cpl)$, hence $H_1(Cpl)$ is not the zero object.
That nonvanishing is the geometric input expected by DetectsNontrivialLinking 3 and by the public-spine gluing at linkingComplementH1. In the Recognition forcing chain this is foundation-level topology (nontrivial linking obstruction), not a T5–T8 constant-forcing step, but it supplies the homology witness those spine lemmas consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.