proj23_apply_coord
plain-language theorem explainer
Coordinate evaluation for the linear projection from R^4 onto the last two axes: as a Fin-2 map it is exactly (y_2, y_3). Anyone simplifying maps built from the flat unknot or its complement retraction will cite this. The proof is pure definitional equality (rfl).
Claim. For every $y\in\mathbb{R}^4$ (Euclidean), the linear projection onto the last two coordinates, read as a map $\mathrm{Fin}\,2\to\mathbb{R}$, equals the pair $(y_2,y_3)$.
background
The module builds the geometric core of nontrivial linking detection in dimension 3: the flat unknot $S^1\hookrightarrow S^3$, $(x_0,x_1)\mapsto(x_0,x_1,0,0)$, a dual circle in the complement, and a continuous retraction of the complement onto that circle.
The projection used throughout is the linear map $\mathrm{proj}_{23}:\mathbb{R}^4\to\mathbb{R}^2$ sending $y\mapsto(y_2,y_3)$ (continuous by finite dimension). Companion inclusions pack $\mathbb{R}^2$ into the first or last two coordinates of $\mathbb{R}^4$. This lemma is the coordinate-level evaluation of that projection, matching the pattern of the sibling evaluation lemmas for the two inclusions.
Everything sits at universe 0 in Mathlib's Euclidean-space and sphere API, ready to glue into the public linking-complement homology spine elsewhere.
proof idea
Term-mode one-liner: rfl. Unfolding the definition of the linear map (its toFun builds WithLp.toLp 2 ![y 2, y 3]) makes the claimed equality of Fin 2 → ℝ maps definitional, so no further rewriting is required. Marked @[simp] for automatic coordinate cleanup.
why it matters
Small but load-bearing simp fact in the unknot-complement retract package that underpins DetectsNontrivialLinking 3. The module's end goal is unknotComplementH1_ne_zero: with $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, the first singular homology of the unknot complement in $S^3$ is nonzero. Coordinate lemmas like this keep the retraction $y\mapsto(y_2,y_3)/|(y_2,y_3)|$ and the dual-circle section algebraically transparent when proving the retraction is the identity on the core and when assembling continuous maps between spheres.
No direct downstream edges are recorded yet; the lemma exists so later continuity, embedding, and homology arguments can reduce projection applications without manual ext/fin_cases noise. It is pure foundation geometry, not a forcing-chain (T0–T8) step, but it supplies the topological substrate those recognition arguments rely on for linking.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.