hypIsometry
plain-language theorem explainer
The orthogonal hyperplane to the north pole of the unit sphere S^{n+1} is linearly isometric to Euclidean R^{n+1}, the ambient space of S^n. Sphere-cover and linking arguments cite this to move between the hyperplane model and standard Euclidean coordinates. The definition is the representation map of the orthonormal basis of that hyperplane obtained from the unit north-pole vector.
Claim. For every natural number $n$, the orthogonal complement of the north-pole ray in Euclidean space $\mathbb{R}^{n+2}$ is linearly isometric (over $\mathbb{R}$) to Euclidean space $\mathbb{R}^{n+1}$.
background
In this module the ambient space of the unit $n$-sphere is Esp n, namely Euclidean space $\mathbb{R}^{n+1}$ with the standard orthonormal frame indexed by Fin (n+1). The north-pole vector is the last standard basis vector; it has unit norm. The north-pole hyperplane Hyp m is the orthogonal complement of the ray through that vector inside Esp m.
The target of the present map is therefore Hyp (n+1), a codimension-one subspace of $\mathbb{R}^{n+2}$, while the codomain is Esp n $\cong \mathbb{R}^{n+1}$. Mathlib supplies OrthonormalBasis.fromOrthogonalSpanSingleton, which builds an orthonormal basis of the orthogonal complement of a nonzero vector once the ambient finite rank is known in the shape finrank = k+1. The local lemma fact_finrank_esp packages exactly that rank fact for Esp (n+1).
proof idea
Install the finite-rank instance via fact_finrank_esp n. Feed the north-pole vector of Esp (n+1) into OrthonormalBasis.fromOrthogonalSpanSingleton. Nonzeroness of that vector is the short chain: if its norm vanished then, by norm_northV, one would equal zero, contradicting one_ne_zero. The resulting orthonormal basis has representation map repr, which is already a linear isometry equivalence from the hyperplane onto EuclideanSpace ℝ (Fin (n+1)), i.e. onto Esp n.
why it matters
This isometry is the linear bridge used by interHomotopyEquiv (Step 2 of the singular-sphere cover argument): after identifying the intersection of the two punctured covers with a punctured hyperplane, sphereHomeoOfLinearIsometryEquiv (hypIsometry n) converts that hyperplane model into the standard sphere $S^n$. The same geometric toolkit supports high-dimensional linking statements in LinkingVanishingHighDim. In the Recognition foundation stack the construction is pure Euclidean geometry; it does not itself invoke the forcing chain T0–T8, but it supplies the sphere models those later topological steps rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.