coord23_eq_zero_of_mem_range
plain-language theorem explainer
Any point of S³ that lies on the flat unknot has vanishing third and fourth Euclidean coordinates. Topologists working the unknot-complement retract cite it to certify that the dual circle misses the unknot. The proof unpacks the range witness and reads off the two zero slots of the linear inclusion (x₀,x₁)↦(x₀,x₁,0,0).
Claim. If $y\in S^3$ lies in the image of the flat unknot $S^1\hookrightarrow S^3$, $(x_0,x_1)\mapsto(x_0,x_1,0,0)$, then the Euclidean coordinates of $y$ satisfy $y_2=0$ and $y_3=0$.
background
The module builds a geometric core for nontrivial linking detection in dimension 3. It defines the flat unknot as the continuous map $S^1\to S^3$ induced by the linear isometry $\mathrm{incl}{01}:\mathbb{R}^2\to\mathbb{R}^4$, $(x_0,x_1)\mapsto(x_0,x_1,0,0)$, together with the dual core circle $\mathrm{incl}{23}:(z_0,z_1)\mapsto(0,0,z_0,z_1)$ valued in the complement.
Points of the Mathlib TopCat spheres are ULifted metric spheres in Euclidean space, so coordinate extraction means reading the underlying EuclideanSpace ℝ (Fin 4) vector. The lemma records the elementary fact that every point of the unknot image has zero in slots 2 and 3, which is exactly the defining formula of $\mathrm{incl}_{01}$.
This is pure point-set topology at universe 0; no homology is invoked yet. The same coordinate language is used later for the retraction of the complement onto the core circle.
proof idea
Term-mode unpacking of the range membership. From $y\in\mathrm{range}(\mathrm{unknot})$ obtain a preimage $w\in S^1$. Congruence along ULift.down and the first component yields $\mathrm{incl}{01}(w)=y$ as Euclidean vectors. Applying congrFun at indices 2 and 3, then simplifying with the definition of $\mathrm{incl}{01}$ (which hard-codes zeros in those slots), gives the two equalities. No external lemmas beyond definitional unfolding.
why it matters
Feeds directly into coreFun, the point-level dual circle. There the lemma is the contradiction engine: if a core point $(0,0,z_0,z_1)$ lay on the unknot, coordinates 2 and 3 would vanish, forcing the unit vector $(z_0,z_1)$ to be zero. That places the core inside the complement Cpl, which is required before the continuous retraction and the identity-on-core check can be stated.
Those pieces assemble into unknotComplementH1_ne_zero, the geometric heart of DetectsNontrivialLinking 3 on the public spine. In the Recognition forcing chain this supplies the topological witness that the eight-tick / $D=3$ linking data is homologically nontrivial, rather than a contractible artifact. The lemma itself is elementary bookkeeping, but without it the core cannot be typed into the complement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.