coverU
plain-language theorem explainer
Open chart on the n-sphere obtained by deleting the south pole. It is one half of the standard two-set cover used for Mayer–Vietoris on S^n (especially S^1). Downstream lemmas treat it as open, contractible, and complementary to the north-pole chart. The body is a one-line set complement.
Claim. For each $n\in\mathbb{N}$, let $S^n$ be the unit sphere in $\mathbb{R}^{n+1}$. Write $s$ for the south pole. Define the open set $U:=S^n\setminus\{s\}$.
background
In this module the n-sphere is realized as the unit sphere in Euclidean space $\mathbb{R}^{n+1}$ (typed as a topological space Sph n). The north pole is the last standard basis vector; the south pole is its negative.
The classical stereographic atlas uses two charts: sphere minus south pole and sphere minus north pole. Their union is the whole sphere, their intersection is the doubly punctured sphere, and each chart is contractible. That is the local setting for Mayer–Vietoris computations of low-degree homology of $S^1$ later in the file.
Upstream, southP is defined as $-$north pole on the unit sphere, so the complement is well-typed as a subset of the sphere carrier.
proof idea
Definitional one-liner: the carrier set is the complement of the singleton ${$south pole$}$ inside the underlying set of the n-sphere. No lemmas are applied; noncomputability is inherited from the sphere construction.
why it matters
This chart is the U-half of the open cover that drives the singular-sphere geometry stack. It feeds openness (isOpen_coverU), the cover identity $U\cup V=S^n$, contractibility of $U$, membership facts for equatorial test points, the homeomorphism of $U\cap V$ onto a punctured hyperplane, and the Mayer–Vietoris argument that $H_1(S^1)\neq 0$ via a nonzero point-difference class.
In the Recognition foundation layer this is pure topological scaffolding: it supplies the geometric cover needed before any RS forcing (T0–T8) or cost identities are invoked. It does not itself encode J-cost or phi; it only prepares the sphere for homology and stereographic arguments used by later foundation results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.