coverU_union_coverV
plain-language theorem explainer
The two standard open charts on the n-sphere, each omitting one pole, jointly cover the whole sphere. Anyone running Mayer-Vietoris on S^n cites this as the cover hypothesis. The proof is a one-line case split: every point is either not the south pole (hence in the first chart) or not the north pole (hence in the second), using that the poles are distinct.
Claim. For every $n \in \mathbb{N}$, if $U$ is the $n$-sphere minus the south pole and $V$ is the $n$-sphere minus the north pole, then $U \cup V = S^n$.
background
The ambient space is the unit sphere $\mathrm{Sph}, n$ in Euclidean space of dimension $n+1$. Two distinguished points are fixed: the north pole and the south pole, which are antipodal and therefore unequal (northP_ne_southP).
The open sets used throughout the module are the two punctured spheres: coverU n is the complement of the south pole, and coverV n is the complement of the north pole. Each is open, and each is contractible via stereographic projection onto a hyperplane (the next block of the module).
This cover is the classical two-set atlas for computing sphere homology by Mayer-Vietoris. The intersection is homotopy-equivalent to the equatorial $S^{n-1}$, which is what produces the suspension isomorphism later in the file.
proof idea
Rewrite equality with the universe as a universal quantification over points of the sphere. Fix an arbitrary point $x$. Case on whether $x$ equals the south pole.
If $x$ is the south pole, place it in the second chart (sphere minus north pole). Membership fails only if $x$ were also the north pole; that contradicts northP_ne_southP. If $x$ is not the south pole, it lies in the first chart by definition of the complement. No topology is used; the argument is pure set membership.
why it matters
This lemma is the cover hypothesis fed to every Mayer-Vietoris connecting map in the module. Downstream it appears in suspensionIso (the isomorphism $H_{k+2}(S^{n+1}) \cong H_{k+1}(S^n)$ built from $\delta$ of the two-punctured cover), in sphere_homology_vanish (Stage D vanishing $H_k(S^n)=0$ for $1\le k\ne n$), and in h1_s1_ne_zero (nonvanishing of $H_1(S^1)$ via exactness and the point-difference class).
In the Recognition Science forcing chain the sphere package underwrites dimensional and periodicity arguments that sit behind T7 (eight-tick octave) and T8 ($D=3$). Without a verified full cover, the MV exact sequences used to force those landmarks would not type-check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.