norm_northV
plain-language theorem explainer
The north-pole vector in Euclidean space of dimension n+1 has unit Euclidean norm. Anyone building the unit sphere point, stereographic charts, or the north-pole hyperplane isometry cites this fact. The proof is a three-step rewrite: unfold the single-basis definition, apply the norm of a standard basis vector, then use that the scalar 1 has norm 1.
Claim. For every natural number $n$, if $e_n$ denotes the last standard basis vector in the Euclidean space $\mathbb{R}^{n+1}$ (the north-pole vector with coefficient $1$), then $\|e_n\| = 1$.
background
In SingularSphereGeometry one works with the unit sphere $S^n$ inside the Euclidean space $\mathrm{Esp},n \simeq \mathbb{R}^{n+1}$. The north-pole vector is the last standard basis vector: a single at $\mathrm{Fin.last},n$ with coefficient $1$. To place that vector on the unit sphere one needs its Euclidean norm to equal $1$.
Mathlib already records that a single basis vector scaled by a real $c$ has norm $|c|$, and that $|1|=1$. This lemma packages those facts for the concrete north-pole choice used by every stereographic and hyperplane construction in the module.
proof idea
Short rewrite proof. Unfold the north-pole vector to a single basis vector with coefficient $1$. Apply EuclideanSpace.norm_single, which reduces the norm of a single to the absolute value of its coefficient. Finish with norm_one, the fact that the real number $1$ has norm $1$.
why it matters
Elementary norm certificate that lets the north pole sit on the unit sphere. The north-pole sphere point is defined by packaging the vector with this identity via the membership criterion that a point lies on the unit sphere about the origin iff its norm is $1$. The same identity feeds the non-vanishing lemma for the north-pole vector, which supplies the nonzero hypothesis for the orthonormal basis that identifies the north-pole hyperplane of $S^{n+1}$ with Euclidean $n$-space. Stereographic projection at the north pole also takes the unit-norm fact as an explicit local hypothesis when restricting charts to the doubly punctured sphere.
In the Recognition foundation layer this is pure Euclidean bookkeeping under the singular-sphere geometry that supports continuum bridges; it is not itself a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.