northP_ne_southP
plain-language theorem explainer
On the unit n-sphere in Euclidean (n+1)-space, the north and south poles are distinct points for every n. Anyone building stereographic charts, two-set open covers, or the S^0 classification cites this separation. The proof is a short contradiction: equality would force the north pole vector to vanish while still having norm one.
Claim. For every natural number $n$, if $N$ denotes the north pole of the unit sphere $S^n \subset \mathbb{R}^{n+1}$ and $S = -N$ the south pole, then $N \neq S$.
background
The ambient space is Euclidean $\mathbb{R}^{n+1}$ (written Esp n), and Sph n is the unit sphere about the origin as a topological space. The north pole is the last standard basis vector, normalized to lie on the sphere; the south pole is defined as its additive inverse on that sphere.
This module sets up the classical two-chart atlas for $S^n$: open sets omitting one pole each, with stereographic projection relating the overlap to a punctured hyperplane. Distinctness of the poles is the elementary geometric fact that makes those charts proper and the cover exhaustive.
Upstream, the argument uses that the Euclidean norm of zero is zero and that $0 \neq 1$ in the scalar field (via the project's choice-free rational nontriviality lemma).
proof idea
Assume for contradiction that the north and south poles coincide as sphere points. Coercion to the ambient Euclidean space and the definition of the south pole give $N = -N$. Adding $N$ yields $2N = 0$, hence $N = 0$ after ruling out the scalar $2 = 0$. But membership in the unit sphere forces $|N| = 1$, so $|0| = 1$, i.e. $0 = 1$, contradiction. The last step invokes the simp lemma that the norm of zero is zero together with scalar nontriviality.
why it matters
Pole separation is the first nontrivial geometric fact in the singular-sphere geometry layer. It is used immediately to prove that the two open charts (sphere minus south pole, sphere minus north pole) cover the whole sphere, and that their intersection is homeomorphic to the punctured hyperplane under stereographic projection. It also feeds the classification that every point of $S^0$ is one of the two poles.
In the Recognition Science foundation stack this geometry underwrites the topological side of the forcing chain (octave structure, dimensional constraints) by giving a clean, Mathlib-aligned model of $S^n$ with named poles. Without distinct poles the chart cover and the punctured-sphere homeomorphism would collapse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.