pathConnected_inter
plain-language theorem explainer
The open intersection of the two standard polar charts on the sphere S^{n+2} (sphere minus both poles) is path-connected. Anyone setting up Mayer–Vietoris or induction for singular homology of spheres would cite this instance. The proof pulls path-connectedness of the punctured hyperplane across the stereographic homeomorphism of that intersection.
Claim. For every natural number $n$, the subspace $U\cap V\subset S^{n+2}$ is path-connected, where $U$ is the sphere minus the south pole and $V$ is the sphere minus the north pole.
background
The module builds the standard two-chart atlas on the unit sphere needed for Stage D vanishing of singular homology. Write $S^{m}$ for the unit sphere in the ambient Euclidean space of the module; the north and south poles are the usual antipodal points on the last axis. The open set coverU m is $S^{m}$ minus the south pole; coverV m is $S^{m}$ minus the north pole. Their union is the whole sphere, and each chart is open.
The intersection $U\cap V$ is the sphere with both poles removed. Stereographic projection identifies it with the punctured hyperplane Hyp m (the equatorial copy of $\mathbb{R}^{m}$ with the origin deleted). The module already records a homeomorphism interHomeoPunctured between that intersection and the punctured hyperplane.
Path-connectedness of the charts and of their intersection is the topological input for Mayer–Vietoris and for the inductive vanishing argument announced just below this declaration: $H_k(S^{n})=0$ for $1\le k$ with $k\ne n$.
proof idea
Fix $n$ and work on dimension $n+2$. First apply Mathlib’s isPathConnected_compl_singleton_of_one_lt_rank to the hyperplane Hyp (n+2) at the origin, using the rank hypothesis one_lt_rank_hyp n (so the ambient dimension is at least 2). Convert the resulting IsPathConnected fact into a PathConnectedSpace instance on the punctured hyperplane.
Then transport that instance across the inverse of interHomeoPunctured (n+2): the inverse is continuous and surjective, so Continuous.surjective.pathConnectedSpace yields path-connectedness of the sphere intersection. The whole argument is a short transfer, not a fresh path construction on the sphere.
why it matters
This instance is Step-2 infrastructure for the Stage D vanishing block in SingularSphereGeometry: the claim $H_k(S^{n})=0$ whenever $1\le k$ and $k\ne n$. Without path-connectedness of $U\cap V$, the Mayer–Vietoris long exact sequence (or the corresponding Čech/nerve argument) does not start cleanly, so the inductive removal of intermediate homology degrees stalls.
In the Recognition Science forcing chain the sphere geometry sits under the dimensional forcing that produces $D=3$ spatial dimensions (T8) and the eight-tick octave (T7). The present lemma is dimension-generic ($n$ arbitrary); the RS-native case is the low-dimensional specialization used when the singular complex is tied to the recognition register. No downstream theorems currently list this instance as a direct edge, so its role is local to the vanishing induction in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.