coreFun
plain-language theorem explainer
Pointwise map sending z on S¹ to the dual core circle (0,0,z₀,z₁) inside the unknot complement in S³. Cited by anyone using the continuous core map or the retraction identity on that circle. Built as a subtype package: embed via the last two coordinates, check unit norm, and exclude the unknot image by a zero-norm contradiction.
Claim. For each point $z$ on the unit circle $S^1$, the assignment $z \mapsto (0,0,z_0,z_1)$ is a point of $S^3$ lying outside the image of the flat unknot $(x_0,x_1)\mapsto(x_0,x_1,0,0)$.
background
The module builds a self-contained geometric model of the unknot complement in $S^3$, matching the shape expected by DetectsNontrivialLinking 3 and the PublicSpine linking witness. The flat unknot is the embedding $S^1\hookrightarrow S^3$ given by $(x_0,x_1)\mapsto(x_0,x_1,0,0)$. Its complement is the TopCat object of points of $S^3$ outside that image.
The dual core circle lives in the complementary coordinate plane: $(0,0,z_0,z_1)$. This definition is the underlying point-set function; the continuous map into the complement is assembled from it one step later. The key upstream fact is that any point in the unknot image has vanishing coordinates 2 and 3, so the two planes meet only at the origin, which is not on $S^3$.
proof idea
Construct a subtype element of the complement. Push $z$'s two coordinates into slots 2 and 3 of Euclidean $\mathbb{R}^4$ via the linear inclusion that zeros the first pair. Unit-norm membership on $S^3$ is immediate: the inclusion preserves norms and $z$ already lies on $S^1$.
To stay out of the unknot image, assume for contradiction membership in the range. The coordinate-extraction lemma then forces both coordinates of $z$ to vanish, so the underlying vector is zero. But the sphere membership of $z$ says its norm equals 1, and rewriting with the zero vector yields $0=1$, a contradiction.
why it matters
This is the point-set engine under the continuous core map into the complement and under the identity theorem that the complement retraction, restricted along the core, recovers the identity on $S^1$. Those two facts together show the unknot complement retracts onto a circle, so its first singular homology is nontrivial.
That homology witness is the geometric content of DetectsNontrivialLinking 3 and is glued elsewhere into the PublicSpine linking-complement argument. In the Recognition forcing chain it supplies the topological reason linking is detected precisely when spatial dimension is three (T8), via an explicit retract rather than an abstract duality appeal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.