incl23
plain-language theorem explainer
The coordinate inclusion of R² into R⁴ that sends (x₀,x₁) to (0,0,x₀,x₁), packaged as a linear isometry. Anyone building the dual core circle in the unknot complement cites it. The body is a direct verification: linearity by coordinate cases, isometry by equating the two Euclidean norms via finite sums of squares.
Claim. The map $(x_0,x_1)\mapsto(0,0,x_0,x_1)$ is a linear isometry $\mathbb{R}^2\to\mathbb{R}^4$ (with the standard Euclidean norms).
background
This module is a standalone Mathlib-only development of the geometric core behind nontrivial linking detection in dimension 3. It constructs the flat unknot $S^1\hookrightarrow S^3$ by $(x_0,x_1)\mapsto(x_0,x_1,0,0)$, its complement, a dual core circle valued in that complement, and a retraction of the complement onto the core. The payoff is that the first singular homology of the unknot complement is nonzero once $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is available.
Euclidean space here is Mathlib's $\ell^2$ product space on a finite index type: points of $\mathbb{R}^n$ with the standard norm. Linear isometries are linear maps that preserve that norm. The present inclusion is the orthogonal partner of the unknot embedding: it places a second copy of $\mathbb{R}^2$ in the last two coordinates of $\mathbb{R}^4$, so the two planes meet only at the origin and the dual circle misses the unknot.
proof idea
The definition builds a LinearIsometry whose underlying linear map sends $x$ to the length-4 tuple $(0,0,x_0,x_1)$ via WithLp.toLp. Additivity and homogeneity are proved by extending equality of coordinates and running fin_cases on the four indices, simplifying with the pointwise PiLp add/smul lemmas. Norm preservation rewrites both sides with EuclideanSpace.norm_eq, expands the finite sums over Fin 4 and Fin 2, and simplifies: the two leading zeros contribute nothing, so $|(0,0,x_0,x_1)|=|x|$.
why it matters
This is the linear-algebraic spine of the dual core circle. Downstream, coreFun applies it to a unit vector in $\mathbb{R}^2$ and lands in the unknot complement; core packages that as a continuous map $S^1\to\mathrm{Cpl}$. The simp lemma on coordinates records the pointwise formula used throughout the retract construction.
In the module narrative this is half of the geometric pair (unknot plane vs core plane) that makes the retraction $y\mapsto(y_2,y_3)/|(y_2,y_3)|$ well-defined on the complement and the identity on the core. That retract, together with $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, yields nonvanishing $H_1$ of the unknot complement in $S^3$, the geometric input later glued into the public linking-complement spine. Within Recognition Science this sits in the Foundation layer supporting DetectsNontrivialLinking in dimension 3 (the forced spatial dimension T8), not in the forcing chain T0–T8 itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.