interHomotopyEquiv
plain-language theorem explainer
The intersection of the two open punctured covers of S^{n+1} (sphere minus each pole) is homotopy equivalent to the equator sphere S^n. Homology computations that run Mayer-Vietoris on the two-hemisphere cover of the sphere cite this equivalence. The construction chains a homeomorphism of the intersection onto a polar product S^n × (0,∞), then contracts the radial ray.
Claim. For every $n \in \mathbb{N}$, writing $U$ and $V$ for the open sets $S^{n+1}$ minus the south pole and $S^{n+1}$ minus the north pole respectively, the intersection $U \cap V$ is homotopy equivalent (as a topological space) to the unit $n$-sphere $S^n$.
background
The ambient space is Euclidean space $\mathbb{R}^{n+1}$ (here Esp n), and $S^n$ is its unit sphere. The two open covers of $S^{n+1}$ are the sphere minus the south pole and the sphere minus the north pole; both are contractible, and their union is the whole sphere.
Their intersection is the sphere with both poles removed. In polar coordinates relative to the axis through the poles, that set is homeomorphic to the equatorial sphere $S^n$ times the open ray $(0,\infty)$ of radial heights. The ray is contractible, so the product is homotopy equivalent to $S^n$ alone.
This module builds the classical suspension isomorphism for singular homology of spheres via Mayer-Vietoris on the two-punctured cover. The present definition is Step 2 of that argument: identify the intersection up to homotopy with the lower-dimensional sphere.
proof idea
Compose four maps. First apply the homeomorphism of the two-pole-punctured sphere onto a standard punctured model (interHomeoPunctured). Next pass to polar coordinates (puncturedPolar), obtaining a product of an $n$-sphere with the open ray $(0,\infty)$. The sphere factor is identified with the unit sphere in Esp n via the linear isometry hypIsometry n (extended by the identity on the ray). Convert the resulting homeomorphism to a homotopy equivalence, then apply hequivProdContractible to kill the contractible ray factor, landing on $S^n$.
why it matters
This is the geometric input to the suspension isomorphism suspensionIso: $H_{k+2}(S^{n+1}) \cong H_{k+1}(S^n)$. That isomorphism is obtained by taking the Mayer-Vietoris connecting map for the two-punctured cover (an iso because each cover is contractible) and post-composing with the homology map induced by the present homotopy equivalence of the intersection with the equator.
In the Recognition Science foundation stack the suspension isomorphism is the inductive engine that computes singular homology of spheres, which in turn feeds the singular-sphere layer used to force discrete geometric structure (eight-tick octave, $D=3$) upstream of the forcing chain. Without a clean homotopy identification of the intersection, the connecting-map argument does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.