Common tight rows of an edge have rank at least $d-1$

Proved

Hirsch.adj_tight_rows_rank

by elmismisimoxhunca · Sep 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

hirsch-conjecturepolytopes

Let $P=\{x\in\mathbb R^d:\langle a_i,x\rangle\le b_i\}$ and let $x,y$ be adjacent (the segment $[x,y]$ is a nontrivial extreme subset of $P$ , the mission's Adj). Then the normals $a_j$ of the rows tight at both $x$ and $y$ span a subspace of dimension at least $d-1$ :

d\le \dim\operatorname{span}\{a_j:\langle a_j,x\rangle=b_j,\ \langle a_j,y\rangle=b_j\}+1.

Otherwise a direction $e$ orthogonal to all common tight normals and not parallel to $y-x$ would let the midpoint of $[x,y]$ move inside $P$ off the segment, contradicting extremality of the edge. Used to bound the combinatorial neighbourhoods in the polar of the Matschke--Santos--Weibel prismatoid $Q_{28}$ .

Formalization Note Submodule.span of the image of the common tight index set; the inequality is stated in $\mathbb N$ with $+1$ on the right so it is meaningful when $d=0$ .

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

open scoped RealInnerProductSpace

Formal statement

namespace Hirsch

theorem adj_tight_rows_rank (d n : ℕ) (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (x y : EuclideanSpace ℝ (Fin d)) (hadj : Adj (Hpoly a b) x y) :
    d ≤ Module.finrank ℝ (Submodule.span ℝ
      (a '' {j | ⟪a j, x⟫ = b j ∧ ⟪a j, y⟫ = b j})) + 1 := by sorry

end Hirsch

View graph

Common tight rows of an edge have rank at least d−1d-1d−1

Common tight rows of an edge have rank at least $d-1$