southP
plain-language theorem explainer
Defines the south pole of the unit n-sphere as the antipode of the north pole in ambient Euclidean space. Downstream cover constructions and contractibility instances cite it as the distinguished puncture. The body is a one-line negation of the already-constructed north pole subtype.
Claim. For each $n \in \mathbb{N}$, the south pole is the point $-N$ of the unit sphere $S^n \subset \mathbb{R}^{n+1}$, where $N$ is the north pole.
background
The ambient space is Esp n, the Euclidean space $\mathbb{R}^{n+1}$ with the standard inner product. The unit sphere is the set of vectors of norm one about the origin. The north pole is already packaged as a subtype element of that sphere (last standard basis vector, norm one).
This module builds the elementary polar geometry needed for open covers of $S^n$: remove one pole, obtain a contractible chart domain. The south pole is the second distinguished point, defined purely as the antipode so that later lemmas can quote coe_neg_sphere and coordinate identities without re-proving membership.
proof idea
One-line definition: subtype negation of the north pole. Lean’s sphere subtype carries a Neg instance, so -northP n is already a point of the unit sphere; no separate norm proof is required.
why it matters
Feeds the standard two-chart atlas: coverU is the sphere minus the south pole, and contractible_coverU obtains contractibility from the singleton-complement fact for spheres. Also used by ambient-coordinate lemmas (amb_southP, amb_southP_zero), the cover-union identity, intersection homeomorphisms, and the doubly-punctured-circle coordinate nonvanishing argument. In the broader Recognition foundation stack this is pure geometric scaffolding for singular-sphere constructions, not a physics claim; it sits under the topological preliminaries that later support forcing-chain geometry rather than under T5–T8 themselves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.