Cpl
plain-language theorem explainer
The open complement of the standard flat unknot inside the 3-sphere, packaged as a topological space. Anyone citing the unknot-complement retraction or the nonvanishing of its first singular homology uses this object as the ambient space. The body is a one-line subtype construction: points of S³ outside the image of the unknot embedding.
Claim. Let $U\colon S^1\hookrightarrow S^3$ be the standard flat unknot $(x_0,x_1)\mapsto(x_0,x_1,0,0)$. Write $\mathrm{Cpl}$ for the topological space $S^3\setminus U(S^1)$, i.e. the set of points of $S^3$ not in the image of $U$, with the subspace topology.
background
This module builds the geometric core of nontrivial linking detection in dimension 3. It works entirely in Mathlib's TopCat at universe 0, matching the shapes expected by the public linking-complement homology interface.
The unknot is the continuous embedding $S^1\to S^3$ sending $(x_0,x_1)$ to $(x_0,x_1,0,0)$. Its image is a closed circle lying in the first two coordinates. The dual circle $z\mapsto(0,0,z_0,z_1)$ lands entirely off that image and will later serve as a deformation retract of the complement.
The present definition simply names the open set of points of $S^3$ that miss the unknot, so that later maps (core inclusion, coordinate projection onto the last two axes, and the radial retraction) can be typed against a single ambient space.
proof idea
Pure definitional construction: form the subtype of the 3-sphere consisting of those points not in the range of the unknot map, then promote that subtype to a TopCat object via TopCat.of. No lemmas are applied; continuity and openness are inherited from the subspace topology on a co-range of a continuous map into a metric sphere.
why it matters
Every subsequent construction in the module is typed over this space: the core circle map into the complement, the $(y_2,y_3)$-coordinate projection, the well-definedness lemma that those coordinates never vanish on the complement, the radial retraction onto the core, and finally the theorem that the first singular homology of the complement is nonzero (given $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$).
That nonvanishing statement is the geometric engine behind DetectsNontrivialLinking 3 and supplies the exact argument shape required by the public linking-complement homology spine. In the broader Recognition forcing chain it underwrites the topological half of the eight-tick / three-dimensional linking story (T7–T8), by exhibiting a concrete nontrivial $H_1$ class forced by the unknot complement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.