incl01
plain-language theorem explainer
The linear isometry embedding the plane into four-space by zero-padding the last two coordinates: (x₀,x₁) ↦ (x₀,x₁,0,0). Anyone assembling the flat unknot S¹ ↪ S³ cites this as the ambient linear skeleton. The definition packages the coordinate formula with a short check that addition, scalar multiplication, and the Euclidean norm are preserved.
Claim. The map $\iota_{01}:\mathbb{R}^2\to\mathbb{R}^4$ defined by $\iota_{01}(x_0,x_1)=(x_0,x_1,0,0)$ is a linear isometry of Euclidean spaces (with the standard $\ell^2$ norms).
background
This standalone module builds the geometric core for nontrivial first singular homology of the unknot complement in $S^3$, the engine behind DetectsNontrivialLinking 3. Ambient spaces are Mathlib Euclidean spaces $\mathbb{R}^2$ and $\mathbb{R}^4$ (finite-dimensional $\ell^2$ products). The flat unknot is the restriction of the first-two-axes inclusion to unit spheres; a dual last-two-axes circle lives in the complement, and radial retraction onto it shows $H_1$ of the complement is nonzero once $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is available.
Everything sits at universe 0 and matches the shapes later glued into the public-spine linking-complement homology statement. No Recognition-native constants ($\varphi$, $J$-cost, rung ladder) appear here; the file imports only Mathlib.
proof idea
Definition of a LinearIsometry, not a tactic proof of a proposition. The underlying linear map sends $x$ to the length-four tuple $(x_0,x_1,0,0)$ via the $\ell^2$ packaging. Additivity and homogeneity are checked by extending over the four coordinates and simplifying with the pointwise sum and scalar rules for product $\ell^p$ spaces. Norm preservation rewrites both Euclidean norms as square roots of summed squares, expands the $\mathrm{Fin},4$ and $\mathrm{Fin},2$ sums, and drops the two zero coordinates.
why it matters
This is the ambient linear map under the pointwise unknot and the continuous unknot $S^1\to S^3$. Downstream facts use it to: extract coordinates (the image is exactly the padded pair); prove the unknot is injective (via injectivity of the linear isometry); and show range points have vanishing last two coordinates, which feeds well-definedness of the dual-part map on the complement. Those pieces assemble the retraction onto the dual circle and the nonvanishing of $H_1$ of the unknot complement. In the Recognition stack this is pure geometric scaffolding for the linking/detection layer, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.