incl01_apply_coord
plain-language theorem explainer
Coordinate evaluation of the linear isometry that embeds ℝ² into ℝ⁴ by zero-padding the last two slots. Anyone normalizing the flat unknot map or its complement retraction will fire this as a simp rule. The proof is pure definitional equality (rfl).
Claim. For every $x \in \mathbb{R}^2$, the image of $x$ under the linear isometry $\mathbb{R}^2 \hookrightarrow \mathbb{R}^4$ given by zero-padding is the 4-tuple $(x_0,x_1,0,0)$, when both sides are read as functions $\mathrm{Fin}\,4\to\mathbb{R}$.
background
This module builds the geometric core for nontrivial linking detection in dimension 3: the flat unknot $S^1\hookrightarrow S^3$, a dual circle in its complement, and a continuous retraction of the complement onto that dual circle. The first singular homology of the complement is then shown nonzero once $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is available.
The supporting map is the linear isometry that sends $(x_0,x_1)$ to $(x_0,x_1,0,0)$ inside Euclidean 4-space (the ambient model for $S^3$). Points of Euclidean space are WithLp vectors; coordinate access is via the underlying Fin n → ℝ function. This lemma records that coordinate view explicitly so later simp steps can rewrite without unfolding the isometry structure.
proof idea
One-line reflexivity. The isometry's underlying linear map is defined by WithLp.toLp 2 ![x 0, x 1, 0, 0]; casting the image back to Fin 4 → ℝ recovers that same array definitionally, so rfl closes the goal.
why it matters
Tiny but load-bearing bookkeeping inside the unknot-complement package that underpins DetectsNontrivialLinking 3 and the public-spine linking homology statement. Without a clean coordinate normal form for the zero-pad inclusion, the embedding proof for the flat unknot, the dual-circle core, and the retraction formulas become noisy. No downstream consumers are wired in this module yet; the gluing to the public spine happens elsewhere. Framework role is geometric infrastructure for the D=3 / eight-tick linking story, not a forcing-chain step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.