one_lt_rank_hyp
plain-language theorem explainer
The real rank of the north-pole orthogonal hyperplane Hyp(n+2) is strictly greater than one. Anyone proving path-connectedness of the stereographic double-cover intersection on spheres of dimension at least two cites this. The argument equates Module.rank with finite rank via finrank_hyp and finishes by a numeric comparison 1 < n+2.
Claim. For every natural number $n$, if $H_{n+2}$ denotes the orthogonal complement of the north-pole ray inside $\mathbb{R}^{n+2}$, then $1 < \mathrm{rank}_{\mathbb{R}}(H_{n+2})$.
background
In SingularSphereGeometry one works with the Euclidean space Esp n and its unit sphere Sph n. The north-pole vector northV n spans a one-dimensional ray; Hyp n is the orthogonal complement of that ray, realized as a submodule of Esp n. Stereographic charts coverU and coverV are built from the two poles, and their intersection is identified with the punctured hyperplane Hyp n \ {0}.
The finite-dimensional rank of that hyperplane is already known: finrank_hyp states Module.finrank ℝ (Hyp (n+1)) = n+1, obtained from the orthogonal-complement formula for a nonzero singleton span once the ambient dimension of Esp is fixed. The present lemma upgrades that equality to a strict lower bound on the (possibly infinite) Module.rank, which is the hypothesis demanded by Mathlib’s path-connectedness criterion for complements of points in real vector spaces.
proof idea
Invoke finrank_hyp at index n+1 to obtain Module.finrank ℝ (Hyp (n+2)) = n+2. Rewrite Module.rank via the identity finrank_eq_rank (valid because the space is finite-dimensional). The numeric inequality 1 < n+2 is discharged by omega and cast into the cardinal comparison.
why it matters
The sole downstream consumer is the instance pathConnected_inter, which shows that coverU(n+2) ∩ coverV(n+2) is path-connected. That instance applies isPathConnected_compl_singleton_of_one_lt_rank precisely to the inequality proved here, then transports path-connectedness along the chart identification. The surrounding module comment labels this “Step 3: path-connectedness of the intersection in dimension ≥ 2”, a prerequisite for the Mayer–Vietoris / singular-homology computation of spheres that underpins the geometric side of the Recognition foundation (eight-tick octave and D = 3 sit downstream of the same sphere package). Without the rank bound the Mathlib path-connectedness lemma does not fire.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.