core
plain-language theorem explainer
The dual circle to the flat unknot: a continuous map $S^1\to S^3\setminus U$ sending $z\mapsto(0,0,z_0,z_1)$. Cited by anyone building the retraction of the unknot complement or proving $H_1$ of that complement is nontrivial. Continuity is packaged from the linear-isometry inclusion of the last two coordinates plus ULift/subtype constructors.
Claim. Let $U\subset S^3$ be the flat unknot $(x_0,x_1)\mapsto(x_0,x_1,0,0)$. The core circle is the continuous map $c:S^1\to S^3\setminus U$ given on points by $c(z)=(0,0,z_0,z_1)$.
background
This module is a Mathlib-only geometric core for DetectsNontrivialLinking 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, then constructs a dual circle valued in the complement and a retraction of that complement onto the dual circle.
Cpl is the unknot complement as a TopCat object: ${x\in S^3:x\notin\mathrm{range}(U)}$, matching the shape expected by the public linking spine. The point-level map coreFun sends $z\mapsto(0,0,z_0,z_1)$ via the linear isometry incl23 (inclusion of the last two Euclidean coordinates) and lands in Cpl because any point of $U$ has vanishing coordinates 2 and 3.
The present declaration lifts that point map to a morphism in TopCat, i.e. a continuous map $S^1\to\mathrm{Cpl}$.
proof idea
Definitional wrapper: toFun is exactly coreFun. Continuity is a short tactic chain. Apply Continuous.subtype_mk twice (once for the complement subtype, once for the sphere subtype), compose with continuous_uliftUp and continuous_uliftDown to move through the universe-0 ULift packaging of TopCat.sphere, and finish with incl23.continuous composed with continuous_subtype_val. No separate continuity lemma is needed beyond the isometry and the subtype/ULift constructors.
why it matters
This is item 3 in the module's six-step program: the dual circle that the complement retracts onto. Downstream in-module results (retractToCore, retract_core, and ultimately unknotComplementH1_ne_zero) need a continuous section of the complement so that $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ injects into the homology of the complement, proving the complement is not acyclic in degree 1.
That nonvanishing is the geometric content behind nontrivial linking detection in three dimensions, aligned with the forcing-chain landmark $D=3$ (T8) and with the public spine's linkingComplementH1 gluing (done elsewhere). Without a continuous core map, the retraction identity and the homology argument have nothing to restrict along.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.