amb_southP
plain-language theorem explainer
The ambient Euclidean coordinates of the south pole on the unit n-sphere equal the negative of the north-pole basis vector. Arguments that need explicit pole coordinates in R^{n+1} (S^0 classification, punctured-circle charts) cite this identity. The proof is a one-line term application of the sphere-coercion lemma for negation.
Claim. For every $n\in\mathbb{N}$, writing $S_n$ for the south pole of the unit sphere in $\mathbb{R}^{n+1}$ and $e_n$ for the last standard basis vector (the north-pole vector), the ambient coordinates of $S_n$ equal $-e_n$.
background
The module equips the unit $n$-sphere as the topological space of unit vectors in the Euclidean space $E_n:=\mathbb{R}^{n+1}$ (indexed by $\mathrm{Fin}(n+1)$). The north-pole vector is the last standard basis vector $e_n$, and the north and south poles are the corresponding unit-sphere points.
The helper amb extracts ambient $E_n$-coordinates from a point of the sphere object (a coercion across the topological-category packaging). South-pole ambient coordinates are therefore the natural dual of the north-pole vector under the sphere embedding.
Local setting is pure sphere geometry: open covers by the two polar charts, and later coordinate non-vanishing on the doubly punctured circle $S^1\setminus{\mathrm{N},\mathrm{S}}$.
proof idea
One-line term proof. Apply the Mathlib sphere-coercion identity for negation at the north pole: the ambient representative of the antipodal (south) pole is exactly the negation of the north-pole vector. No further rewriting is required.
why it matters
Feeds three in-module lemmas. First, the $S^0$ dichotomy: every point of the $0$-sphere is one of the two poles, which uses the ambient form of the south pole to reduce the unit-norm equation in $\mathbb{R}^1$ to $\pm 1$. Second, the coordinate identity that the $0$-th ambient component of the south pole on $S^1$ vanishes. Third, non-vanishing of the first ambient coordinate on the doubly punctured circle, which underwrites the polar chart cover.
In the Recognition foundation stack this is scaffolding for singular-sphere geometry used downstream of the forcing chain (eight-tick octave, $D=3$), not a physics claim itself. It closes the elementary pole-coordinate bookkeeping needed before chart and cover arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.