contractibleSpace_compl_singleton_sphere
plain-language theorem explainer
Any unit sphere in a real inner product space remains contractible after deleting one point. The argument is a three-step homeomorphism chain through stereographic projection onto the orthogonal hyperplane of the removed ray, which is a topological vector space. Algebraic topologists cite it to equip the standard two-chart cover of S^n with contractible charts, and it feeds the formal Hatcher arc-complement acyclicity argument.
Claim. Let $E$ be a real inner product space and let $p$ be a point of the unit sphere $S = \{x \in E : \|x\| = 1\}$. Then the punctured sphere $S \setminus \{p\}$, with the subspace topology, is a contractible space.
background
Work in a real normed space $E$ carrying an inner product. The unit sphere $S = \mathrm{sphere}(0,1)$ is the set of vectors of norm one. Stereographic projection from a point $p \in S$ is the standard chart that sends $S \setminus {p}$ homeomorphically onto the orthogonal hyperplane $(\mathbb{R}\cdot p)^\perp \subset E$.
A real topological vector space is contractible: the straight-line homotopy $H(t,v) = (1-t)v$ retracts it onto the origin. Consequently any space homeomorphic to such a hyperplane is contractible. The module builds the two open charts coverU and coverV on the singular sphere by deleting the south and north poles respectively; each chart is exactly a punctured sphere of this form.
(The recorded depends-on edges naming an adjacency Finset E are name collisions with the type parameter and play no role in the argument.)
proof idea
Term-mode homeomorphism chain. First record $|p|=1$ from membership in the sphere. Identify the set-theoretic complement ${p}^c$ with the source of Mathlib's stereographic hp by setCongr. Compose with the chart homeomorphism toHomeomorphSourceTarget from source to target. Identify the target with the full orthogonal hyperplane $(\mathbb{R}\cdot p)^\perp$ via stereographic_target and Homeomorph.Set.univ. The composite homeomorphism transfers contractibility of the hyperplane (as a real TVS) back to the punctured sphere.
why it matters
Immediate consumers are the instances contractible_coverU and contractible_coverV, which specialise the theorem at the south and north poles and equip the standard two-set open cover of the singular sphere with contractible charts. Those charts are the geometric input to the Mayer–Vietoris / nerve arguments that establish arc-complement acyclicity (arcComplementsAcyclic): every embedded arc in $S^D$ has $H_1$-acyclic complement (Hatcher 2B.1, arc case). The bisection lemma bad_step sits in the same development.
In the Recognition foundation layer this is pure topology scaffolding: it supplies the contractible opens needed before any forcing-chain or eight-tick content appears. It does not itself force $D=3$ or invoke the J-cost; it only clears the homotopy-type ground so later singular-sphere geometry can run.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.