northP
plain-language theorem explainer
The north pole of the unit n-sphere is the point whose ambient vector is the last standard basis vector in Euclidean (n+1)-space. Anyone building stereographic covers, pole-punctured spheres, or linking arguments on S^n cites this. Construction is a subtype package: the north-pole vector together with the already-proved unit-norm fact.
Claim. For each $n \in \mathbb{N}$, the north pole is the point of the unit sphere $S^n = \{x \in \mathbb{R}^{n+1} : \|x\|=1\}$ given by the last standard basis vector $e_n = (0,\ldots,0,1)$.
background
The ambient space is Euclidean $\mathbb{R}^{n+1}$ (indexed by $\mathrm{Fin}(n+1)$). The unit $n$-sphere sits inside it as the set of vectors of norm one. The north-pole vector is the last standard basis vector: the Dirac mass at the final coordinate with value $1$.
A companion lemma already records that this vector has Euclidean norm exactly $1$. The present definition lifts that vector into the subtype of points of the sphere (center $0$, radius $1$). The south pole is obtained later by negation of the same point.
Local setting is the geometry of the singular sphere used for open covers, contractibility of punctured charts, and intersection homotopy type in the Foundation layer.
proof idea
One-line subtype constructor. The ambient vector is the north-pole vector; membership in the unit sphere is discharged by rewriting through the zero-center sphere criterion (norm equals radius) and applying the unit-norm lemma for that vector.
why it matters
Canonical basepoint for the sphere geometry stack. Downstream it defines the open cover chart that is the sphere minus the north pole, and supplies the singleton whose complement is contractible. South-pole identities are obtained by coe-negation of this point. Coordinate nonvanishing on the doubly punctured circle, ambient-coordinate evaluations, and east/west pole separation in the linking-vanishing high-dimension module all route through it. In the Recognition foundation this is pure geometric scaffolding for continuum and homotopy arguments, not a forcing-chain step (T0–T8) itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.