unknot
plain-language theorem explainer
The flat unknot is the continuous map S¹ → S³ sending (x₀,x₁) to (x₀,x₁,0,0) in the TopCat model of spheres. Anyone proving nontrivial linking or complement homology in dimension 3 cites it as the concrete embedded circle. Continuity is assembled by composing the linear inclusion of the first two coordinates with the ULift and subtype structure maps.
Claim. The standard flat unknot is the continuous map $S^1 \to S^3$ given on underlying points by $(x_0,x_1)\mapsto(x_0,x_1,0,0)$, packaged as a morphism of $\mathbf{Top}$ spheres at universe $0$.
background
This module builds the geometric core for nontrivial linking detection in $S^3$. It works entirely in Mathlib's TopCat spheres at universe 0: unit spheres in Euclidean space $\mathbb{R}^2$ and $\mathbb{R}^4$, wrapped by ULift so the shapes match the public spine's linking-complement homology functor.
The linear isometry that pads two coordinates by zeros, $(x_0,x_1)\mapsto(x_0,x_1,0,0)$, is the geometric inclusion of the first plane into $\mathbb{R}^4$. The point-level unknot applies that inclusion to a point of $S^1$ and re-packages the image as a point of $S^3$, using that the inclusion preserves norms so the unit sphere is preserved.
The local goal is then to treat this map as a continuous morphism of topological spaces, so that its range, complement, and a retraction of the complement onto a dual circle can be formed inside TopCat.
proof idea
Definitional packaging: the underlying function is the already-constructed point-level unknot. Continuity is a short composition chain: continuous ULift down, continuous subtype value, continuous linear inclusion of the first two coordinates, continuous subtype packaging into the target sphere, then continuous ULift up. No separate analytic estimate is needed beyond continuity of those structure maps and of the inclusion.
why it matters
This is item (1) of the module's geometric core for DetectsNontrivialLinking 3. Downstream, the detection theorem exhibits exactly this map together with the embedding proof and the nonvanishing of $H_1$ of its complement: the complement retracts onto the dual circle $(0,0,z_0,z_1)$, so $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ injects into the complement homology and cannot be zero.
That detection half fills the d3_detects field of the Alexander linking bridge on the public spine, the content-typed binder that records a real (non-encoded) linking obstruction in dimension 3. The same map defines the unknot complement object and feeds coordinate lemmas (vanishing of the last two coordinates on the image) used to build the retraction.
In the broader Recognition forcing chain this is the concrete geometric witness behind the $D=3$ linking half of the spine, not an arithmetic encoding of linking.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.