pt2_zero
plain-language theorem explainer
The zeroth coordinate of the Euclidean plane point with real coordinates $(a,b)$ is exactly $a$. Coordinate-extraction lemmas and any argument that reduces vector equalities componentwise would cite this. The proof is definitional reflexivity after unfolding the $L^2$ embedding of the two-vector.
Claim. For all $a,b\in\mathbb{R}$, if $p$ is the point of the Euclidean plane with coordinates $(a,b)$, then the zeroth coordinate of $p$ equals $a$.
background
The ambient space is the Euclidean plane realized as an $L^2$ product space (Esp 1), i.e. $\mathbb{R}^2$ with the standard norm. The helper pt2 builds that point from a pair of reals by packing them into a length-two vector and coercing into the $L^2$ type: the doc-comment states it is "the point of the plane with coordinates $(a,b)$".
This module develops vanishing of linking-type invariants in high dimension, importing singular-sphere geometry and the low-dimensional linking-vanishing results. Coordinate projections of plane points are the elementary bookkeeping needed before one can talk about arcs, complements, and homology of linking configurations.
proof idea
One-line definitional proof: after unfolding the packing of $(a,b)$ into the $L^2$ vector, the zeroth entry is definitionally $a$, so reflexivity closes the goal. Marked @[simp] so the simplification engine can discharge such projections automatically.
why it matters
Tiny but necessary coordinate identity inside the high-dimensional linking-vanishing development. Sibling lemmas (pt2_one, pt2_norm, pt2_mem_sphere, arc-function coordinate facts) build the same local toolkit; together they let later arguments treat plane points by components when checking acyclicity of arc complements or nontrivial linking detection. No downstream consumers are recorded yet, and the lemma does not itself touch the T0–T8 forcing chain, RCL, or $\varphi$-ladder; it is pure Euclidean bookkeeping supporting the geometric side of the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.