twoPunctHomeo
plain-language theorem explainer
Stereographic projection from a base point p on the unit n-sphere restricts to a homeomorphism between the doubly punctured sphere and the equatorial hyperplane minus the image of the second puncture. High-dimensional linking arguments cite it as the chart step before translating the remaining puncture to the origin. The body assembles forward and inverse chart maps, verifies they stay off the punctures, and packages continuity into a single Homeomorph.
Claim. For $n \in \mathbb{N}$ and distinct points $p,q$ on the unit sphere $S^n \subset \mathbb{R}^{n+1}$, stereographic projection $\sigma_p$ from $p$ induces a homeomorphism $S^n \setminus \{p,q\} \simeq_t H_p \setminus \{\sigma_p(q)\}$, where $H_p = (\mathbb{R}\cdot p)^\perp$ is the hyperplane orthogonal to the ambient vector of $p$.
background
The ambient space is Euclidean space $\mathbb{R}^{n+1}$ (written Esp n), and $S^n$ is its unit sphere as a topological space. Each sphere point carries ambient coordinates of unit norm; stereographic projection from a unit vector is the standard chart sending the sphere minus that pole onto the orthogonal hyperplane.
The local module builds high-dimensional vanishing of linking by reducing two-point sphere complements to lower-dimensional spheres. An upstream lemma records that every point other than the chosen pole lies in the stereographic source: the chart is defined precisely off that pole.
This definition generalizes a one-puncture chart homeomorphism to an arbitrary second puncture $q \neq p$, landing in the hyperplane minus the single point $\sigma_p(q)$.
proof idea
Fix the stereographic chart $\varphi$ at the ambient unit vector of $p$. Source membership for every $x \neq p$ is the upstream lemma stereographic_source_pt; the target is the whole hyperplane.
Build a Homeomorph from an underlying Equiv. Forward: apply $\varphi$ to the sphere point and check the image is not $\varphi(q)$ by injectivity of $\varphi$ on the source. Inverse: apply $\varphi^{-1}$ and check the result avoids both $p$ (source of the chart) and $q$ (right-inverse identity). Left and right inverses are the chart identities on source and target, lifted through subtypes.
Continuity of both directions is continuous-on composition of the chart (resp. its inverse) with the subtype valuation, restricted to the open complements.
why it matters
Parent consumer is twoPointComplHEquiv: the two-point complement is homotopy equivalent to the equator sphere, $S^{n+1}\setminus{p,q}\simeq_h S^n$. That construction chains this homeomorphism with a translation of the remaining puncture to the origin, polar coordinates, and collapse of the ray factor.
In the Recognition foundation layer this is pure topology supporting linking-vanishing statements used when high-dimensional sphere complements must be acyclic or homotopy-simple. It does not itself touch the forcing chain (T0–T8), the J-cost, or the eight-tick octave; it is infrastructure for the geometric side of those arguments.
No open scaffold remains: the definition is complete and noncomputable only because stereographic charts are.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.