northV
plain-language theorem explainer
The north-pole vector in the ambient Euclidean space of the n-sphere is the last standard basis vector (last coordinate 1, others 0). Sphere-geometry and stereographic-chart arguments cite it as the distinguished axis for poles, covers, and the orthogonal hyperplane. The body is a one-line Mathlib single-basis constructor.
Claim. For each $n\in\mathbb{N}$, write $E_n=\mathbb{R}^{n+1}$ for the ambient Euclidean space of $S^n$. The north-pole vector is the last standard basis vector $e_n\in E_n$, i.e. the unique vector with last coordinate $1$ and all other coordinates $0$.
background
The module builds the geometry of the unit sphere $S^n$ inside Euclidean space, with poles and stereographic charts as the main tools. The ambient space is abbreviated $E_n:=\mathrm{EuclideanSpace},\mathbb{R},(\mathrm{Fin}(n+1))$, so coordinate indices run over ${0,\ldots,n}$.
The north-pole vector is the distinguished axis used to define the north pole on the sphere, the south pole as its negative, the open covers that omit each pole, and the orthogonal hyperplane at the north pole. Downstream lemmas normalize it and promote it to a point of the unit sphere.
Upstream, the type is exactly that ambient space abbreviation; the last index is Mathlib's terminal element of $\mathrm{Fin}(n+1)$.
proof idea
Pure definition: apply Mathlib's EuclideanSpace.single at the last index of $\mathrm{Fin}(n+1)$ with value $1$. No proof obligations beyond the type of the ambient space.
why it matters
This vector is the geometric seed for the whole pole-and-chart apparatus in SingularSphereGeometry. Immediate dependents include the unit-norm lemma, the north-pole point on $S^n$, the orthogonal hyperplane at that pole, and the stereographic homeomorphism from the doubly punctured sphere onto the punctured hyperplane (south pole to the origin). Ambient-coordinate lemmas for the south pole and the nonvanishing first coordinate on the doubly punctured circle also rewrite through it.
In the broader Recognition foundation, singular-sphere geometry supports the topological side of the forcing chain (octave structure, dimensional constraints). The definition itself is inert scaffolding: the content lives in the norm, pole, cover, and homeomorphism results that quote it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.