Adjacency of two vertices is the common-tight-row face being the segment

Proved

Hirsch.spindle_adj_iff_common_tight_face

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

hirsch-conjecturepolytopessantos-counterexample

Let $K=\{x\in\mathbb R^m:\langle A_i,x\rangle\le B_i\}$ be a bounded H-polytope with all $B_i>0$ (so the origin is strictly feasible) and let $x,y$ be vertices. Then $x,y$ are adjacent (the segment $[x,y]$ is an extreme subset, the mission's Adj) if and only if $x\ne y$ and the face cut out by the rows tight at both $x$ and $y$ ,

\{z\in K:\ \langle A_i,z\rangle=B_i\ \text{whenever } \langle A_i,x\rangle=B_i=\langle A_i,y\rangle\},

is exactly the segment $[x,y]$ .

Direction $\Leftarrow$ : an equality set of valid inequalities is extreme. Direction $\Rightarrow$ : at the midpoint $w$ of $[x,y]$ the tight rows are precisely the common tight rows; for any $z$ in the displayed face, a short extension $w+\tau(w-z)$ stays in $K$ (all other rows have positive slack at $w$ ), so $w$ lies strictly between $z$ and a point of $K$ , and extremality of $[x,y]$ forces $z\in[x,y]$ . This is the elementary 'smallest face containing two vertices' fact, stated without any face-lattice machinery; it is the basic tool for transporting adjacency along perturbations in the strong $d$ -step argument.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

open scoped RealInnerProductSpace
open WithLp EuclideanSpace

Formal statement

namespace Hirsch

theorem spindle_adj_iff_common_tight_face
    (m N : ℕ) (A : Fin N → EuclideanSpace ℝ (Fin m))
    (B : Fin N → ℝ) (hB : ∀ i, 0 < B i)
    (hbd : Bornology.IsBounded (Hpoly A B))
    (x y : EuclideanSpace ℝ (Fin m))
    (hx : x ∈ Set.extremePoints ℝ (Hpoly A B))
    (hy : y ∈ Set.extremePoints ℝ (Hpoly A B)) :
    Adj (Hpoly A B) x y ↔
      x ≠ y ∧
      {z | z ∈ Hpoly A B ∧ ∀ i,
        ⟪A i, x⟫ = B i → ⟪A i, y⟫ = B i → ⟪A i, z⟫ = B i}
        = segment ℝ x y := by sorry

end Hirsch

Source

F. Santos, A counterexample to the Hirsch conjecture, Annals of Math. 176 (2012), arXiv:1006.2814, Section 2 (Lemma 2.2 'pushing', Lemma 2.4, proof of Theorem 2.6 last paragraph); B. Matschke, F. Santos, C. Weibel, arXiv:1202.4701, Lemma 2.15. Primal transcription: campaign plan ~/hirsch-campaign/plans/spindle_axis_plan_astra.md (2026-09-06).

View graph