perpIsometry
plain-language theorem explainer
At any point p on the unit sphere S^{n+1}, the orthogonal hyperplane to the ray through p is linearly isometric to Euclidean n-space. Anyone building stereographic charts or two-point complement homotopy equivalences on spheres cites this. The construction is a one-line application of the orthonormal-basis representation of the orthogonal complement of a unit vector.
Claim. For every $n\in\mathbb{N}$ and every point $p$ on the unit sphere $S^{n+1}\subset\mathbb{R}^{n+2}$, there is a linear isometry $(\mathbb{R}\cdot p)^{\perp}\simeq_{\ell i}\mathbb{R}^{n+1}$ between the orthogonal hyperplane to the ambient position vector of $p$ and the ambient Euclidean space of $S^{n}$.
background
The ambient space of the $n$-sphere is $\mathrm{Esp},n:=\mathrm{EuclideanSpace},\mathbb{R},(\mathrm{Fin}(n+1))$, i.e. $\mathbb{R}^{n+1}$ with the standard Euclidean structure. Sphere points live in the unit sphere of that space; amb simply reads off the underlying ambient vector. The orthogonal complement $(\mathbb{R}\cdot v)^{\perp}$ of a nonzero vector $v$ is then a codimension-one subspace of $\mathrm{Esp}(n+1)$.
The module sits in the high-dimensional linking-vanishing development: one needs flexible charts and complement models at arbitrary base points, not only at the north pole. An earlier special case (hypIsometry) treats only the north-pole hyperplane; the present definition removes that restriction.
Upstream, fact_finrank_esp packages the rank identity $\mathrm{finrank},\mathrm{Esp}(n+1)=n+2$ in the shape required by Mathlib's orthonormal-basis constructor, and unit-norm of sphere points (norm_amb) guarantees the spanning vector is nonzero.
proof idea
Install the finrank fact fact_finrank_esp n as an instance. Feed the ambient vector of $p$ to Mathlib's OrthonormalBasis.fromOrthogonalSpanSingleton at dimension $n+1$; the nondegeneracy side-condition is discharged by rewriting the assumed zero-norm through norm_amb and norm_zero, then invoking one_ne_zero. The resulting orthonormal basis of the orthogonal complement supplies its representation map .repr, which is the desired linear isometric equivalence onto $\mathrm{Esp},n$.
why it matters
This isometry is the movable-base-point upgrade of the north-pole hyperplane chart. Downstream it is consumed by twoPointComplHEquiv, whose doc-comment states the goal: the two-point complement is homotopy equivalent to the equator sphere, $S^{n+1}\setminus{p,q}\simeq_h S^n$ for distinct $p,q$, via stereographic projection at $p$, translation of the image of $q$ to the origin, polar coordinates, and collapse of the ray factor.
In the Recognition foundation stack this supplies the geometric engine for high-dimensional linking vanishing: once two-point complements are standard spheres, linking and homology obstructions in high dimension reduce to ordinary sphere topology. It does not itself touch the forcing chain (T0–T8) or the J-cost calculus; it is pure Euclidean sphere geometry supporting those later topological arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.