pt2_one
plain-language theorem explainer
The second Cartesian coordinate of the plane point with entries (a, b) is exactly b. Coordinate-extraction simp fact used wherever plane points are built via the two-slot embedding. Proof is definitional reflexivity.
Claim. For all real $a,b$, if $p$ is the point of the Euclidean plane with coordinates $(a,b)$, then the coordinate of $p$ at index $1$ equals $b$.
background
The ambient object is the Euclidean plane realized as an $\ell^2$ product space. The constructor pt2 (documented as "the point of the plane with coordinates $(a,b)$") packs a pair of reals into that space via the standard two-slot vector.
This module develops vanishing of linking data in high dimension, importing singular-sphere geometry and the low-dimensional linking-vanishing companion. Coordinate projections on plane points are the elementary bookkeeping layer beneath arc and sphere constructions that appear later in the same file.
proof idea
One-line wrapper: the statement is definitional. Unfolding the plane-point constructor yields the literal second slot of the two-vector, so reflexivity closes the goal. Marked @[simp] so later tactics can rewrite the second coordinate automatically.
why it matters
Infrastructure lemma inside the high-dimensional linking-vanishing development. It pairs with the companion first-coordinate fact and the norm/sphere-membership lemmas on the same constructor, keeping coordinate algebra out of the geometric arguments. No downstream theorem currently cites it directly; it is local simp support for plane-point calculations that feed arc-complement and linking-detection statements in the module. Not itself a forcing-chain step (T0–T8), but part of the geometric substrate those arguments use when dimensions rise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.