unknotFun
plain-language theorem explainer
Point-set map realizing the flat unknot $S^1\to S^3$ by zero-padding: $(x_0,x_1)\mapsto(x_0,x_1,0,0)$, on universe-0 metric spheres. Anyone citing the continuous TopCat unknot or the complement retract chain uses this as the underlying function. Construction applies the linear isometry incl01 and checks the image stays on the unit sphere via norm preservation.
Claim. Define $f:S^1\to S^3$ on the unit spheres in $\mathbb{R}^2$ and $\mathbb{R}^4$ by $f(x_0,x_1)=(x_0,x_1,0,0)$, transported through universe-$0$ $\mathrm{ULift}$ wrappers. Equivalently, apply the linear isometry that pads two trailing zeros and retain the sphere membership certificate.
background
This module is a Mathlib-only geometric core for nontrivial linking detection in dimension 3. It builds the flat unknot as a continuous map $C(S^1,S^3)$, proves it is an embedding, constructs the dual circle in the complement, and exhibits a retraction of the complement onto that circle, so that $H_1$ of the unknot complement is nonzero once $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is available.
The linear isometry incl01 is the ambient map $\mathbb{R}^2\to\mathbb{R}^4$, $(x_0,x_1)\mapsto(x_0,x_1,0,0)$. Metric spheres here are unit spheres centered at the origin in Euclidean space. Universe-0 ULift wrappers match the shapes expected by the public linking-complement spine elsewhere in the monolith.
The continuous TopCat-level unknot is assembled from this point map plus a continuity proof; embedding and complement homology sit further downstream in the same file.
proof idea
Term-mode definition. Unpack the input point from ULift, apply incl01 to the underlying vector in $\mathbb{R}^2$, and repackage into a subtype of the unit sphere in $\mathbb{R}^4$ under ULift.up. Sphere membership is discharged by rewriting with mem_sphere_zero_iff_norm and incl01.norm_map (isometries preserve norms), then invoking the input sphere certificate. No tactics beyond that short by block.
why it matters
This is the raw point function underneath the continuous flat unknot $S^1\hookrightarrow S^3$ in the module. The parent definition unknot sets toFun := unknotFun and only has to prove continuity. That continuous map is item (1) in the module's geometric core for DetectsNontrivialLinking 3: embedding, dual core circle, complement retraction, and the nonzero $H_1$ statement all sit on top of it.
In the broader Recognition spine this supplies the classical unknot model whose complement carries nontrivial first homology, the topological input later glued into linkingComplementH1 on the public spine. It is pure classical topology (no RS constants, no forcing chain), but it is the geometric witness the linking detector needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.