retract_core
plain-language theorem explainer
The retraction of the unknot complement in S³ onto its dual core circle is the identity when restricted along that core: every point of S¹ is fixed. Anyone citing the pure-retraction proof that H₁ of the unknot complement is nontrivial needs this identity. The argument is a short coordinate computation: the (y₂,y₃)-projection of the core recovers the original unit vector, so normalizing does nothing.
Claim. For every $z\in S^1$, the composition of the core embedding $S^1\to S^3\setminus U$ (sending $z\mapsto(0,0,z_0,z_1)$) with the radial retraction of the unknot complement onto that core circle equals $z$. Equivalently, the retraction restricted along the core is $\mathrm{id}_{S^1}$.
background
This module is a standalone Mathlib-only development of the geometric core behind nontrivial linking detection in dimension 3. The flat unknot is the embedding $U:S^1\hookrightarrow S^3$ given by $(x_0,x_1)\mapsto(x_0,x_1,0,0)$. Its complement $Cpl=S^3\setminus\mathrm{range}(U)$ carries a dual circle, the core map, sending $z\in S^1$ to $(0,0,z_0,z_1)$ (valued in the complement because the first two coordinates vanish only off the unknot).
The retraction of the complement onto that core is the continuous map that keeps only the last two coordinates and renormalizes: $y\mapsto(y_2,y_3)/|(y_2,y_3)|$. The auxiliary projection part23 extracts exactly those last two Euclidean coordinates from a point of $Cpl$. The present identity says the core is a section of that retraction.
The shapes match those used later by the public-spine linking-complement homology interface; gluing is deferred to another module.
proof idea
Fix $z\in S^1$. First prove that the $(y_2,y_3)$-part of the core image equals the underlying unit vector of $z$: extend equality of Fin-2 vectors and discharge both coordinates by fin_cases plus simplification of the definitions of the part, core, and core point-map. Next record that this underlying vector already has Euclidean norm 1 (sphere membership). After peeling the ULift and Subtype wrappers, the goal is that normalizing part23(core z) recovers $z$'s vector; rewrite with the two facts above, then inv_one and one_smul finish.
why it matters
This is item 5 in the module's geometric checklist and the only nontrivial algebraic identity needed before the continuous-map form of the section equation. Immediately downstream, retract_comp_core packages the pointwise identity as equality of continuous maps retractToCore ∘ core = id. That section equation is what the capstone unknotComplementH1_ne_zero quotes: core and the retraction exhibit $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ as a retract of $H_1$ of the unknot complement, so the latter cannot be the zero object in ModuleCat ℤ.
In the broader Recognition spine this supplies the geometric half of DetectsNontrivialLinking 3 and feeds the public-spine linking-complement $H_1$ interface. It is pure classical topology (no RS constants), but it is the concrete reason the eight-tick / $D=3$ linking story can detect nontriviality via homology rather than by hand-waving.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.