amb
plain-language theorem explainer
Extracts the underlying Euclidean vector of a point on the unit n-sphere, undoing the TopCat packaging of Sph. Anyone writing coordinate identities, arc maps, or injectivity arguments on S^n cites this coercion. The body is a one-line subtype projection x.1.
Claim. For any $n \in \mathbb{N}$ and any point $x$ of the unit sphere $S^n \subset \mathbb{R}^{n+1}$ (viewed as a topological space), $\mathrm{amb}(x)$ is the underlying vector of $x$ in the ambient Euclidean space $\mathbb{R}^{n+1}$.
background
The ambient space Esp n is EuclideanSpace ℝ (Fin (n+1)), i.e. ℝ^{n+1} with the standard Euclidean structure. Sph n packages the unit sphere sphere(0,1) in that space as an object of TopCat via TopCat.of, so a point of Sph n is a subtype element whose first component is a vector of norm 1.
Working with coordinates, norms, or maps out of the sphere therefore needs a routine way to recover that vector. The module SingularSphereGeometry sets up poles, open covers, and related geometry on this packaged sphere; amb is the shared coercion used throughout those constructions and in the high-dimensional linking-vanishing development that builds on them.
proof idea
Definitional abbreviation only: amb x is the subtype projection x.1 from the carrier of TopCat.of (sphere 0 1) back into Esp n. No lemmas or tactics are involved.
why it matters
This is the workhorse coercion for every coordinate calculation on Sph. Downstream, LinkingVanishingHighDim uses it to define arcParam (t = (1 - amb z 0)/2), to state the circle equation amb z 0² + amb z 1² = 1, to expand arcFun in coordinates, and to prove arcMap_injective and arcFun_arcParam via amb_injective and coordinate comparison.
In the Recognition foundation stack, singular-sphere geometry supports linking and vanishing arguments that feed dimensional and topological constraints (including the D = 3 forcing chain). Without a uniform ambient projection, those identities would repeatedly re-open the TopCat wrapper by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.