Esp
plain-language theorem explainer
Ambient Euclidean space R^{n+1} carrying the unit n-sphere in the SingularSphereGeometry development. Anyone citing sphere topology, arc-complement acyclicity, or linking-vanishing results in this library uses this type as the host space. The declaration is a one-line noncomputable abbreviation of Mathlib's EuclideanSpace.
Claim. For each natural number $n$, write $E^{n}$ for the Euclidean space $\mathbb{R}^{n+1}$ (inner-product space with orthonormal basis indexed by $\{0,\ldots,n\}$). This is the ambient space in which the unit $n$-sphere $S^{n}$ is realized.
background
The module SingularSphereGeometry fixes a concrete model of spheres for Recognition Science foundation work: the unit sphere in a finite-dimensional real Euclidean space. Mathlib supplies EuclideanSpace ℝ (Fin (n+1)), the unique (up to isometry) real inner-product space of dimension $n+1$ with the standard orthonormal frame.
Sibling abbreviations build on this host: Sph n is the unit sphere about the origin in that space, with distinguished north and south poles and the usual open stereographic covers. Downstream topology (T2 instances, embeddings, orthogonal hyperplanes) is inferred from the Euclidean structure.
The local setting is classical differential topology of spheres, used later to import Hatcher-style complement acyclicity into the RS forcing and ledger geometry stack.
proof idea
Pure definitional abbreviation: Esp n is definitionally equal to Mathlib's EuclideanSpace ℝ (Fin (n + 1)). No proof obligations; noncomputable is inherited from the Mathlib Euclidean construction.
why it matters
This type is the ambient carrier for essentially all sphere geometry in the foundation layer. Downstream it appears in arc-complement acyclicity (every embedded interval in $S^D$ has $H_1$-acyclic complement), the circle-complement reduction via Mayer-Vietoris, homeomorphisms between TopCat and Sph models of complements, embedding lemmas for arc maps, and the orthogonal-hyperplane isometry that drops dimension by one.
Those results feed linking-vanishing statements used to control topological obstructions in high-dimensional recognition geometry. Within the broader RS chain they support clean sphere models once $D=3$ is forced (T8) and eight-tick octave structure is in place, without committing yet to the physical constants or mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.