northV_ne_zero
plain-language theorem explainer
The north-pole vector in Euclidean space of dimension n+1 is nonzero. Sphere-geometry and homology arguments cite it whenever they need a genuine spanning direction for the orthogonal hyperplane. The proof is a one-line wrapper: unit norm of the pole contradicts the norm of zero via one ≠ zero.
Claim. For every natural number $n$, the north-pole vector $e_n \in \mathbb{R}^{n+1}$ (the last standard basis vector) satisfies $e_n \neq 0$.
background
In SingularSphereGeometry, Euclidean space Esp n is the ambient real inner-product space of dimension $n+1$, and the unit sphere Sph n sits inside it. The north-pole vector is defined as the last standard basis vector: northV n := EuclideanSpace.single (Fin.last n) 1. Its Euclidean norm is identically one (norm_northV).
The lemma is elementary linear algebra, but it is the nondegeneracy hypothesis required by Mathlib's formula for the finite rank of the orthogonal complement of a singleton span. Upstream, one_ne_zero is the Peano fact $1 \neq 0$, and norm_zero is the simp rule $|0|=0$. Together they convert a vector-equality assumption into a numeric contradiction.
proof idea
One-line wrapper. Assume northV n = 0. Rewrite via norm_northV so that $|\mathrm{northV}, n|=1$ becomes $|0|=1$, then apply norm_zero to obtain $1=0$, which is exactly the negation of one_ne_zero.
why it matters
Feeds finrank_hyp, the rank computation Module.finrank ℝ (Hyp (n+1)) = n+1. That lemma applies Mathlib's Submodule.finrank_orthogonal_span_singleton and needs a nonzero generator; this is the generator. The hyperplane rank is the base algebraic input for the inductive homology vanishing argument on spheres in the same module (the $S^0$ base case and the path-connectedness step for dimensions $\ge 2$). In the Recognition foundation this geometry underwrites the singular-sphere scaffolding used when dimension and covering data are forced (cf. T8, $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.