incl23_apply_coord
plain-language theorem explainer
Coordinate form of the linear isometry that embeds the plane into R^4 by zero-padding the first two slots: incl23(x) reads as [0,0,x0,x1]. Anyone simplifying maps built from the dual circle in the unknot complement cites this. The proof is pure definitional equality (rfl).
Claim. For every $x\in\mathbb{R}^2$ (Euclidean), the linear isometry that sends $x$ to $(0,0,x_0,x_1)\in\mathbb{R}^4$, when viewed as a map $\mathrm{Fin}\,4\to\mathbb{R}$, equals the coordinate vector $[0,0,x_0,x_1]$.
background
The module builds the geometric core of nontrivial linking detection in dimension 3: the flat unknot $S^1\hookrightarrow S^3$, its complement, a dual circle valued in that complement, and a retraction of the complement onto the dual circle. All constructions live in Euclidean spaces of dimensions 2 and 4 (with the usual identification of $S^3$ as the unit sphere in $\mathbb{R}^4$).
The upstream map is the linear isometry $\mathrm{incl}_{23}:\mathbb{R}^2\to\mathbb{R}^4$ given by $(x_0,x_1)\mapsto(0,0,x_0,x_1)$. It is the raw embedding used to place the dual circle in the last two coordinates, complementary to the unknot which lives in the first two. This lemma simply exposes that embedding at the level of coordinate functions $\mathrm{Fin},4\to\mathbb{R}$.
proof idea
One-line wrapper: the statement is definitionally true from the toFun clause of incl23 (which builds WithLp.toLp 2 ![0, 0, x 0, x 1]), so the proof is rfl. The @[simp] attribute makes the coordinate form fire automatically in later goals.
why it matters
Supports the dual-circle and retraction constructions that feed unknotComplementH1_ne_zero, the module's main homology nonvanishing result. That nonvanishing is the geometric engine behind DetectsNontrivialLinking 3 and the public-spine gluing into linkingComplementH1. Without a clean coordinate simp rule, every subsequent identity involving the dual circle would re-expand the linear-isometry definition by hand. No direct T0–T8 landmark is touched here; the lemma is pure geometric scaffolding for the linking/homology side of the foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.