Hyp
plain-language theorem explainer
Defines the north-pole hyperplane in the ambient Euclidean space of the n-sphere: the orthogonal complement of the real span of the last standard basis vector. Sphere-geometry and stereographic-projection arguments cite it as the codomain for polar charts and punctured-sphere homeomorphisms. The body is a one-line type abbreviation, not a proof.
Claim. For each $n \in \mathbb{N}$, write $E_n = \mathbb{R}^{n+1}$ with the standard Euclidean structure and let $v_N$ be the last standard basis vector. Then $\mathrm{Hyp}(n)$ is the orthogonal complement $( \mathbb{R} \cdot v_N )^\perp \subseteq E_n$, viewed as a real submodule (hence a Euclidean subspace of dimension $n$).
background
The module works in the standard model of the unit $n$-sphere inside Euclidean space. The ambient space $E_n$ is EuclideanSpace ℝ (Fin (n+1)), i.e. $\mathbb{R}^{n+1}$ with the usual inner product. The north-pole vector $v_N$ is the last standard basis vector (the point with a single $1$ in the final coordinate).
Orthogonal complement is taken in the submodule lattice of $E_n$: the real line through $v_N$ is spanned, then its orthogonal is extracted. That hyperplane is the natural linear model for the stereographic chart at the north pole and for the polar decomposition of the punctured hyperplane.
Local setting is singular-sphere geometry: open covers omitting north and south poles, stereographic homeomorphisms, and path-connectedness of double intersections used later for homology vanishing arguments.
proof idea
Pure definitional abbreviation. The type is the orthogonal complement submodule $(\mathbb{R}\cdot v_N)^\perp$ inside $E_n$, coerced to a Type. No tactics or lemmas fire; Mathlib's submodule orthogonal and span-singleton constructors supply the carrier.
why it matters
This hyperplane is the linear stage on which the rest of the singular-sphere toolkit sits. Downstream, hypIsometry exhibits an isometric linear equivalence $\mathrm{Hyp}(n+1)\simeq E_n$, so the north-pole hyperplane of $S^{n+1}$ is identified with the ambient space of $S^n$. interHomeoPunctured restricts stereographic projection to a homeomorphism from the doubly punctured sphere onto the punctured hyperplane. puncturedPolar then splits that punctured hyperplane as unit sphere times $(0,\infty)$.
Finite-rank and rank lemmas (finrank_hyp, one_lt_rank_hyp) feed the path-connectedness instance on the double cover intersection in dimension $\ge 2$, which is the geometric input to positive-degree homology vanishing for spheres. In the broader Recognition forcing chain this is pure geometric scaffolding (sphere covers, not yet T5–T8), but it underwrites the topological side of the eight-tick and dimensional arguments that later force $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.