Sph
plain-language theorem explainer
The n-sphere is packaged as a topological space object: the unit sphere about the origin in Euclidean (n+1)-space. Algebraic topologists working the arc-complement acyclicity argument cite it as the ambient sphere S^D. The definition is a one-line wrapper that lifts Mathlib's metric sphere into TopCat.
Claim. For each $n \in \mathbb{N}$, write $\mathrm{Sph}(n)$ for the topological space given by the unit sphere $\{ x \in \mathbb{R}^{n+1} : \|x\| = 1 \}$ (equivalently, the sphere of radius $1$ about the origin in Euclidean space of dimension $n+1$), viewed as an object of the category of topological spaces.
background
The ambient Euclidean space is the abbreviation $\mathrm{Esp}(n) := \mathrm{EuclideanSpace},\mathbb{R},(\mathrm{Fin}(n+1))$, i.e. $\mathbb{R}^{n+1}$ with the standard Euclidean structure. Mathlib already supplies the metric sphere sphere c r as a subtype of that space; here the center is the origin and the radius is $1$.
The module packages singular-sphere geometry used by the foundation layer: poles, stereographic covers, and closed segments on $S^n$. Downstream work treats $\mathrm{Sph}(D)$ as the ambient sphere in which arcs embed, so that complements and their singular homology can be formed inside $\mathbf{Top}$.
The target type is TopCat (topological spaces as a category), so open/closed sets, embeddings, and homology functors apply uniformly without leaving the categorical interface.
proof idea
One-line definitional wrapper: form Mathlib's unit sphere sphere (0 : Esp n) 1 and coerce it into TopCat via TopCat.of. No lemmas are proved; noncomputability is inherited from the Euclidean-space infrastructure.
why it matters
This is the ambient sphere for the arc-complement acyclicity theorem (Hatcher 2B.1, arc case): every topological embedding of the unit interval into $S^D$ has $H_1$-acyclic complement in every dimension $D$. That theorem, and the supporting bisection apparatus (Bad, bad_step, badSeq, closed segments, Mayer-Vietoris half-bounds), all quantify over subspaces of $\mathrm{Sph}(D)$ and need a single named TopCat object.
In the Recognition Science foundation stack this supplies the topological $S^D$ against which linking and vanishing statements are stated. It is infrastructure rather than a forcing-chain step (T0-T8), but it is the concrete sphere those homology arguments inhabit when dimension $D$ is fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.