twoPointComplHEquiv
plain-language theorem explainer
The complement of any two distinct points on the sphere $S^{n+1}$ is homotopy equivalent to the equator sphere $S^n$. Anyone computing homology or linking of sphere complements cites this reduction. The proof is a composite of stereographic projection, puncture translation, polar coordinates, a linear isometry of the orthogonal hyperplane, and collapse of a contractible ray.
Claim. For every $n\in\mathbb{N}$ and every pair of distinct points $p,q\in S^{n+1}$, there is a homotopy equivalence $S^{n+1}\setminus\{p,q\}\simeq_h S^n$.
background
Work is in the Euclidean sphere $S^{n+1}\subset E^{n+2}$ (written Sph (n+1) over the ambient Euclidean space Esp). Stereographic projection from a basepoint $p$ identifies the once-punctured sphere with the orthogonal hyperplane $p^\perp$. Removing a second point $q\neq p$ cuts that hyperplane at the stereographic image of $q$.
The local toolkit supplies four maps: twoPunctHomeo (stereographic restriction to the doubly punctured sphere), punctTranslateHomeo (translate the remaining puncture to the origin), perpIsometry (identify $p^\perp$ with $E^n$ by an orthogonal linear isometry), and the product homeomorphism of the punctured hyperplane with $S^{n-1}\times(0,\infty)$ in polar coordinates. The open ray $(0,\infty)$ is contractible, so hequivProdContractible erases that factor up to homotopy.
The module sits in the high-dimensional half of the linking-vanishing development: once complements reduce to ordinary spheres, ordinary sphere homology controls the linking groups.
proof idea
The definition is a pure composite of homeomorphisms, then promoted to a homotopy equivalence and composed with a product-collapse.
Start with twoPunctHomeo (n+1) p q, sending $S^{n+1}\setminus{p,q}$ onto $p^\perp$ minus the stereographic image of $q$. Compose punctTranslateHomeo to move that image to the origin. Apply the polar homeomorphism of the punctured hyperplane with the unit sphere times the positive ray. Transport the sphere factor across perpIsometry n p (and leave the ray fixed). Convert the resulting homeomorphism to a homotopy equivalence, then compose hequivProdContractible to kill the contractible ray factor, landing on $S^n$.
why it matters
The sole recorded consumer is isZero_h2_twoPointCompl, which concludes $H_2(S^n\setminus{p,q})=0$ for $n\ge 1$, $n\neq 3$, by transporting the ordinary vanishing of sphere homology across the isomorphism induced by this equivalence. That vanishing statement is the high-dimensional half of the linking package: nontrivial two-point linking is confined to the classical $S^3$ case (Hopf), matching the Recognition forcing step T8 that singles out $D=3$ spatial dimensions.
Without a clean homotopy model for the two-point complement, the homology argument would have to rebuild stereographic and polar reductions at every call site. Packaging them once here keeps the vanishing theorems short and dimension-uniform outside the Hopf dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.