proj23
plain-language theorem explainer
Linear projection ℝ⁴ → ℝ² that keeps only the last two coordinates. It is the algebraic backbone of the dual-circle retraction on the unknot complement in S³. Anyone citing the geometric core of DetectsNontrivialLinking 3 needs this map. The definition is the coordinate extraction; additivity and homogeneity are discharged by finite case analysis on Fin 2.
Claim. The map $\pi_{23}:\mathbb{R}^4\to\mathbb{R}^2$ defined by $\pi_{23}(y)=(y_2,y_3)$ is an $\mathbb{R}$-linear map between Euclidean spaces (with the $\ell^2$ product structure).
background
The module builds the geometric core of 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 circle valued in that complement, and a continuous retraction of the complement onto the dual circle.
Points of ambient space are modeled as EuclideanSpace ℝ (Fin 4), i.e. $\mathbb{R}^4$ with the $\ell^2$ norm. The dual circle lives in the last two coordinates, so one needs a clean linear projection onto those coordinates before normalizing. Continuity of the projection is free in finite dimension and is recorded separately.
The only external dependency is ordinary Mathlib linear-algebra infrastructure; the listed F2Power edge is incidental and not used in the mathematical content of this map.
proof idea
Definition of a LinearMap by supplying toFun as the coordinate pair $(y_2,y_3)$ packaged via WithLp.toLp 2. Additivity is proved by extending over the two output indices and simplifying with the pointwise addition rule on PiLp. Scalar homogeneity is the same pattern with the pointwise scalar-multiplication rule. No external lemmas beyond Mathlib simp lemmas for product spaces.
why it matters
This projection is the first algebraic step toward the retraction $y\mapsto(y_2,y_3)/|(y_2,y_3)|$ of the unknot complement onto the dual circle. Downstream, part23 applies it to complement points, proj23_apply_coord exposes the coordinate formula for rewriting, and proj23_continuous records continuity so the normalized retraction is continuous.
That retraction, together with the identity-on-core fact, feeds the singular-homology argument that $H_1$ of the unknot complement in $S^3$ is nontrivial. The module is the standalone geometric engine glued later into linkingComplementH1 on the public spine, which is the topological half of DetectsNontrivialLinking 3 in the Recognition forcing chain (the D=3 landmark T8 and the eight-tick octave sit upstream of the linking detection story).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.