pt2_mem_sphere
plain-language theorem explainer
If real coordinates a and b satisfy a² + b² = 1, the corresponding plane point lies on the unit circle in Euclidean R². Geometers building paths on S¹ cite this to place coordinate pairs on the sphere subtype. The proof rewrites sphere membership as unit norm, applies the explicit Euclidean norm of the coordinate point, and uses √1 = 1.
Claim. Let $a,b\in\mathbb{R}$ with $a^2+b^2=1$. Then the point of the Euclidean plane with coordinates $(a,b)$ lies on the unit sphere centered at the origin in $\mathbb{R}^2$ (equivalently, on the unit circle $S^1$).
background
The ambient space is Esp 1, the Euclidean space $\mathbb{R}^2$ (abbreviation for EuclideanSpace ℝ (Fin 2)). Points are built by pt2 a b, which packs coordinates $(a,b)$ into that $L^2$ space. The companion lemma pt2_norm records $|\mathrm{pt2},a,b| = \sqrt{a^2+b^2}$.
The module develops linking-vanishing geometry in high dimensions, importing singular sphere geometry and the low-dimensional linking package. Here the local task is elementary: certify that coordinate pairs on the algebraic circle are genuine points of the metric unit sphere, so they can be used as values of continuous maps into the sphere subtype.
Sphere membership at the origin is equivalent to unit Euclidean norm; that is the bridge between the algebraic hypothesis $a^2+b^2=1$ and the topological sphere.
proof idea
Term-mode rewrite chain. First replace membership in the sphere of radius 1 about 0 by the norm condition $|\cdot|=1$. Substitute the closed form $|\mathrm{pt2},a,b|=\sqrt{a^2+b^2}$ from pt2_norm. The hypothesis $a^2+b^2=1$ collapses the radicand, and $\sqrt{1}=1$ finishes.
why it matters
Feeds the semicircle path arcFun, which maps $t\mapsto(1-2t,,s\sqrt{1-(1-2t)^2})$ into the sphere subtype of $S^1$ and needs exactly this membership certificate in its subtype constructor. That arc is part of the linking-vanishing toolkit in high dimensions: continuous arcs on spheres used to probe whether linking classes survive or die.
In the Recognition foundation layer this is pure geometric scaffolding (sphere geometry supporting later topological constraints), not a forcing-chain step (T5–T8) or a constants identity. It closes a small but mandatory hole so arc constructions typecheck without sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.