Tilting one row through an edge: vertex labels, graph contraction, and the first-step landing

Proved

Hirsch.spindle_edge_split_label_graph

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

hirsch-conjecturepolytopessantos-counterexample

Let $K=\mathrm{Hpoly}(A,B)\subseteq\mathbb R^m$ be bounded with $B_i>0$ ; let $p,q$ be adjacent vertices on row $r$ , $z$ a vertex with row $r$ slack, $h$ a direction with $\langle h,p\rangle<0<\langle h,q\rangle$ , and $c$ the point of $[p,q]$ with $\langle h,c\rangle=0$ . Assume every vertex of $K$ on row $r$ other than $p,q$ has exactly $m$ tight rows, and that the rows other than $r$ tight at $c$ have kernel contained in $\ker A_r$ and meeting $\ker h$ trivially. Replace $A_r$ by $A_r+s\,h$ . Then for all sufficiently small $s>0$ : $c$ and $z$ are vertices of the tilted polytope, and there is a map $\varphi$ from its vertices other than $c$ to vertices of $K$ with $\varphi(z)=z$ , sending edges between such vertices to edges of $K$ or points, and sending every neighbour of $c$ to $p$ or $q$ .

This is the geometric crux of Santos' strong $d$ -step theorem: the tilt creates the new vertex $c$ in the interior of the old edge $[p,q]$ , and the last claim is his observation that 'the first step out of the new facet lands on a facet at the same distance as before'. The proof uses finite determinant certificates for the tilt size: bases singular at $s=0$ give constant branches whose old face has only non-simple vertices on row $r$ , hence lies in $[p,q]$ ; rank analysis of common tight rows yields the edge statements.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

open scoped RealInnerProductSpace
open WithLp EuclideanSpace

Formal statement

namespace Hirsch

theorem spindle_edge_split_label_graph
    (m N : ℕ) (A : Fin N → EuclideanSpace ℝ (Fin m))
    (B : Fin N → ℝ) (r : Fin N)
    (p q c z h : EuclideanSpace ℝ (Fin m))
    (hB : ∀ i, 0 < B i)
    (hbd : Bornology.IsBounded (Hpoly A B))
    (hp : p ∈ Set.extremePoints ℝ (Hpoly A B))
    (hq : q ∈ Set.extremePoints ℝ (Hpoly A B))
    (hz : z ∈ Set.extremePoints ℝ (Hpoly A B))
    (hpq : Adj (Hpoly A B) p q)
    (hrp : ⟪A r, p⟫ = B r) (hrq : ⟪A r, q⟫ = B r)
    (hrz : ⟪A r, z⟫ < B r)
    (hhp : ⟪h, p⟫ < 0) (hhq : 0 < ⟪h, q⟫)
    (hc : c ∈ segment ℝ p q) (hhc : ⟪h, c⟫ = 0)
    (hsimple : ∀ x ∈ Set.extremePoints ℝ (Hpoly A B),
      ⟪A r, x⟫ = B r → x ≠ p → x ≠ q →
      (Finset.univ.filter (fun i : Fin N => ⟪A i, x⟫ = B i)).card = m)
    (hdel : ∀ e : EuclideanSpace ℝ (Fin m),
      (∀ i, i ≠ r → ⟪A i, c⟫ = B i → ⟪A i, e⟫ = 0) →
      ⟪A r, e⟫ = 0 ∧ (⟪h, e⟫ = 0 → e = 0)) :
    ∃ η : ℝ, 0 < η ∧ ∀ s : ℝ, 0 < s → s < η →
      let As := fun i => if i = r then A i + s • h else A i
      c ∈ Set.extremePoints ℝ (Hpoly As B) ∧
      z ∈ Set.extremePoints ℝ (Hpoly As B) ∧
      ∃ φ : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin m),
        φ z = z ∧
        (∀ x ∈ Set.extremePoints ℝ (Hpoly As B), x ≠ c →
          φ x ∈ Set.extremePoints ℝ (Hpoly A B)) ∧
        (∀ x y, x ≠ c → y ≠ c → Adj (Hpoly As B) x y →
          φ x = φ y ∨ Adj (Hpoly A B) (φ x) (φ y)) ∧
        (∀ x, Adj (Hpoly As B) c x → φ x = p ∨ φ x = q) := 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