contractible_coverU
plain-language theorem explainer
The open chart consisting of the unit n-sphere with the south pole removed is a contractible topological space. Anyone building stereographic charts or checking that the two-set cover of the sphere is good for Čech or homotopy arguments will cite this. The proof is a one-line specialization of the general fact that any punctured sphere is contractible.
Claim. For every $n \in \mathbb{N}$, the subspace $S^n \setminus \{\text{south pole}\}$ of the unit sphere in the Euclidean space of dimension $n+1$ is a contractible topological space.
background
The module sets up the standard two-chart cover of the unit sphere $S^n \subset E^{n+1}$ used for singular-sphere geometry. The south pole is the antipode of a fixed unit north vector; the north pole is that vector itself. The set coverU is defined as the complement of the south pole in $S^n$, and coverV is the complement of the north pole. Both are open and their union is the whole sphere.
Upstream, any sphere with a single point removed is contractible: stereographic projection from the removed point is a homeomorphism onto the orthogonal hyperplane, which is a real topological vector space and therefore contractible. That general lemma is stated for an arbitrary point of the unit sphere in any real inner-product space.
proof idea
One-line wrapper. Instantiate the general punctured-sphere contractibility theorem at the south pole of $S^n$. Because coverU n is definitionally the complement of that point, the instance of ContractibleSpace on the subtype follows immediately.
why it matters
Contractibility of each chart is the elementary topological input needed before one can treat the two-set cover of the sphere as a good cover (acyclic intersections, vanishing higher Čech cohomology, or elementary homotopy arguments). In the Recognition Science foundation layer this sits inside the singular-sphere geometry used to support later forcing and dimensional arguments; the eight-tick octave and $D=3$ steps ultimately rely on clean sphere topology, though this particular instance is not yet referenced by a downstream theorem in the graph. It closes the contractibility side of the south-pole chart so that later cover lemmas can assume it as an instance rather than reprove it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.