proj23_continuous
plain-language theorem explainer
The coordinate projection from Euclidean 4-space onto the last two axes is continuous. Anyone building the unknot-complement retraction in S^3 cites this as the continuity of the linear map that extracts those coordinates. The proof is a one-line wrapper of Mathlib's finite-dimensional continuity for linear maps.
Claim. The linear map $\mathbb{R}^4 \to \mathbb{R}^2$ given by $(y_0,y_1,y_2,y_3) \mapsto (y_2,y_3)$ is continuous (with the standard Euclidean topologies).
background
This 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 dual circle. The retraction normalizes the last two coordinates, so one first needs a continuous projection onto those coordinates.
The projection in question is the linear map $\mathrm{proj}{23}:\mathbb{R}^4\to\mathbb{R}^2$ with $\mathrm{proj}{23}(y)=(y_2,y_3)$, packaged as a Mathlib LinearMap between Euclidean spaces. Its doc-comment states it is continuous by finite dimension. Continuity of the full retraction later composes this map with subtype and Ulift projections on the unknot complement.
proof idea
One-line wrapper: apply Mathlib's continuous_of_finiteDimensional to the linear map proj23. No extra algebraic work; finite-dimensional real linear maps between Euclidean spaces are automatically continuous.
why it matters
Feeds part23_continuous, which asserts continuity of the same projection after restricting to the unknot complement (via subtype and Ulift). That lemma is a step toward the continuous retraction of the complement onto the dual circle, and ultimately toward unknotComplementH1_ne_zero: the first singular homology of the unknot complement in $S^3$ is nonzero once $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is available.
In the broader Recognition spine this is pure topology scaffolding for DetectsNontrivialLinking 3 and the public linking-complement $H_1$ interface. It does not itself invoke the forcing chain (T0–T8), the J-cost, or $\varphi$; it only supplies a continuous coordinate extraction used by the geometric retract.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.