norm_amb
plain-language theorem explainer
Every point of the unit n-sphere has ambient Euclidean norm one. Geometers building stereographic charts, orthogonal hyperplanes, and two-point complements on spheres cite this as the basic membership fact. The proof is a one-line wrapper around the Mathlib sphere-membership norm identity.
Claim. For every natural number $n$ and every point $x$ of the unit $n$-sphere in Euclidean space $\mathbb{R}^{n+1}$, the Euclidean norm of the ambient coordinate vector of $x$ equals $1$.
background
The module develops singular sphere geometry used by Recognition Science foundation arguments on linking and vanishing in high dimension. The $n$-sphere is the topological space underlying the unit sphere centered at the origin in Euclidean space of dimension $n+1$ (written $\mathrm{Esp},n$). Points of this TopCat object are subtypes of ambient vectors of length one.
The abbreviation that recovers ambient coordinates extracts the underlying vector from a sphere point, bridging the TopCat.of packaging so that norms and inner products can be computed in the ambient Euclidean space. By definition the sphere is sphere(0,1), so membership already encodes unit length; the ambient-coordinate map is only the coercion helper that surfaces that vector.
proof idea
One-line wrapper applying the Mathlib lemma norm_eq_of_mem_sphere to the sphere point $x$. That lemma states that any point of the metric sphere of radius $1$ about the origin has Euclidean norm $1$; the subtype witness carried by $x$ supplies the membership hypothesis, and the ambient-coordinate coercion is definitionally the underlying vector.
why it matters
This is the workhorse identity every downstream sphere calculation needs once ambient coordinates appear. The high-dimensional linking-vanishing module uses it to prove the circle equation for coordinates, to guarantee that the radial vector of an arbitrary base point is nonzero when building the orthogonal hyperplane isometry, and to feed stereographic charts at arbitrary points (including the two-puncture homeomorphism and the two-point-complement homotopy equivalence $S^{n+1}\setminus{p,q}\simeq_h S^n$). Within the same module it supports pole characterizations and nonvanishing of the first coordinate on the doubly punctured circle. Those facts sit under the structural parent that $S^{n+1}$ minus two points is homotopy-equivalent to the equator sphere, part of the foundation layer's linking-vanishing apparatus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.