finrank_hyp
plain-language theorem explainer
The real finite rank of the north-pole orthogonal hyperplane in Euclidean space of dimension n+2 is exactly n+1. Sphere-geometry and homology arguments cite it when identifying that hyperplane with the ambient space of S^n. The proof installs the ambient finrank Fact and applies the orthogonal-complement rank formula for a nonzero singleton span.
Claim. For every natural number $n$, $\mathrm{finrank}_{\mathbb{R}}(H_{n+1})=n+1$, where $H_{n+1}$ is the orthogonal complement (in Euclidean space $\mathbb{R}^{n+2}$) of the one-dimensional subspace spanned by the north-pole vector.
background
In this module the ambient space of the $n$-sphere is $\mathrm{Esp},n:=\mathrm{EuclideanSpace},\mathbb{R},(\mathrm{Fin}(n+1))$, so $\mathrm{Esp},(n+1)\cong\mathbb{R}^{n+2}$. The north-pole vector is the last standard basis vector; it is nonzero because its norm is one.
The hyperplane $\mathrm{Hyp},m$ is defined as the orthogonal complement of the real span of that north-pole vector inside $\mathrm{Esp},m$. Thus $\mathrm{Hyp},(n+1)$ is a codimension-one subspace of $\mathbb{R}^{n+2}$. The upstream fact fact_finrank_esp packages $\mathrm{finrank}_{\mathbb{R}}(\mathrm{Esp},(n+1))=n+2$ in the Fact shape expected by Mathlib's orthogonal-span lemmas.
Locally the development builds charts and covers on singular spheres; finite rank of these hyperplanes is the linear-algebra input to path-connectedness and homology comparisons in dimension $\ge 2$.
proof idea
Term-mode proof. First introduce the instance
Fact (finrank ℝ (Esp (n+1)) = n+1+1) by applying fact_finrank_esp n (which unwraps finrank_euclideanSpace_fin). Then invoke Mathlib's Submodule.finrank_orthogonal_span_singleton on the nonzero north-pole vector of $\mathrm{Esp},(n+1)$, supplied by northV_ne_zero (n+1). The orthogonal complement of a one-dimensional span therefore has finrank $(n+2)-1=n+1$.
why it matters
Immediate consumer is one_lt_rank_hyp, which rewrites finrank to rank and concludes $1<\mathrm{rank}_{\mathbb{R}}(\mathrm{Hyp},(n+2))$ by a trivial arithmetic comparison. That rank lower bound is the linear-algebra gate for path-connectedness of chart intersections on spheres of dimension $\ge 2$ in the singular-sphere geometry development.
In the Recognition foundation this sits under the geometric scaffolding that supports the eight-tick / $D=3$ forcing chain (T7–T8): sphere topology and its homology must be available in Lean before those dimension-forcing steps can be stated cleanly. The lemma itself is pure Euclidean linear algebra; its value is that it closes the finrank side of the hyperplane–sphere identification used throughout the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.