unknot_injective
plain-language theorem explainer
The flat unknot map $S^1\to S^3$, $(x_0,x_1)\mapsto(x_0,x_1,0,0)$, is injective on points. Anyone proving it is a topological embedding, or building the unknot-complement $H_1$ argument for nontrivial linking in dimension 3, cites this. The proof peels ULift and subtype wrappers, then uses injectivity of the linear inclusion $\mathbb{R}^2\hookrightarrow\mathbb{R}^4$.
Claim. The continuous map $u:S^1\to S^3$ defined by $u(x_0,x_1)=(x_0,x_1,0,0)$ (the standard flat unknot) is injective: if $u(a)=u(b)$ then $a=b$.
background
This module is a Mathlib-only geometric core for DetectsNontrivialLinking 3. It builds the flat unknot as a continuous map of TopCat spheres, shows it is an embedding, constructs a dual core circle in the complement, and retracts the complement onto that circle, so that $H_1$ of the complement is nonzero once $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is known.
The unknot itself is the continuous map whose underlying function composes the linear isometry $\mathrm{incl}_{01}:\mathbb{R}^2\to\mathbb{R}^4$, $(x_0,x_1)\mapsto(x_0,x_1,0,0)$, with the sphere subtype and universe-lift wrappers that match the shapes used later by the public linking spine. Injectivity of that map is the missing algebraic step before the embedding theorem can fire: continuous injective maps from compact spaces into Hausdorff spaces are embeddings.
proof idea
Tactic proof on points $a,b$ of the domain sphere with $u(a)=u(b)$. Congruence on the composite (down-project the ULift, then take the first subtype component) yields $\mathrm{incl}{01}(a\downarrow)=\mathrm{incl}{01}(b\downarrow)$. Linear-isometry injectivity of $\mathrm{incl}_{01}$ recovers equality of the $\mathbb{R}^2$ coordinates. ULift.ext and Subtype.ext reassemble that into $a=b$. No topology is used; only the point-set structure of the sphere encoding.
why it matters
Feeds directly into unknot_isEmbedding, whose doc-comment states the unknot is a topological embedding as a continuous injective map from a compact space to a Hausdorff space. That embedding is the first of six geometric facts the module exports; together they show the unknot complement in $S^3$ has nontrivial first singular homology, the geometric engine behind nontrivial linking detection in dimension 3.
In the Recognition foundation stack this is pure topology scaffolding: it does not invoke the forcing chain T0–T8, the J-cost, or $\varphi$, but it supplies the concrete $S^1\hookrightarrow S^3$ model that the public spine later glues to ledger-level linking statements. Closing injectivity here keeps the complement-retract path free of sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.