Length increment for a prepared spindle under a small tilt

Proved

Hirsch.spindle_prepared_no_short_apex_walk

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

hirsch-conjecturepolytopessantos-counterexample

Let $P=\mathrm{Hpoly}(a,b)\subseteq\mathbb R^d$ be a bounded spindle with apices $u,v$ , $b_i>0$ , row $k$ tight at $v$ , row $j$ tight at $u$ with the rows tight at $u$ other than $j$ still spanning, every vertex other than $u,v$ row-simple, and no padded walk of length $d$ from $u$ to $v$ . Form the symmetric wedge over $k$ and tilt row $j$ to $\langle a_j,x\rangle+\varepsilon t\le b_j$ . Then there is $\eta>0$ such that for every $0<\varepsilon<\eta$ there is no padded walk of length $d+1$ from $(u,0)$ to $(v,0)$ in the tilted polytope.

This is Santos' Theorem 2.6 length increment in the primal. A padded $(d+1)$ -walk from $(u,0)$ is followed from its last visit to $(u,0)$ : the next vertex is labelled $p$ or $q$ (the two lifts of $u$ ) by the edge-split lemma, the remaining at most $d$ steps map to a walk in the untilted wedge, and the wedge projection turns that into a padded walk of length $\le d$ from $u$ to $v$ in $P$ , contradicting the hypothesis.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

open scoped RealInnerProductSpace
open WithLp EuclideanSpace

Formal statement

namespace Hirsch

theorem spindle_prepared_no_short_apex_walk
    (d n : ℕ) (a : Fin n → EuclideanSpace ℝ (Fin d))
    (b : Fin n → ℝ) (k j : Fin n)
    (u v : EuclideanSpace ℝ (Fin d)) (hb : ∀ i, 0 < b i)
    (hbd : Bornology.IsBounded (Hpoly a b))
    (hu : u ∈ Set.extremePoints ℝ (Hpoly a b))
    (hv : v ∈ Set.extremePoints ℝ (Hpoly a b))
    (hsp : ∀ i, (⟪a i, u⟫ = b i) ↔ ⟪a i, v⟫ ≠ b i)
    (hk : ⟪a k, v⟫ = b k) (hj : ⟪a j, u⟫ = b j)
    (hdel : ∀ e : EuclideanSpace ℝ (Fin d),
      (∀ i, i ≠ j → ⟪a i, u⟫ = b i → ⟪a i, e⟫ = 0) → e = 0)
    (hsimple : ∀ x ∈ Set.extremePoints ℝ (Hpoly a b),
      x ≠ u → x ≠ v →
      (Finset.univ.filter (fun i : Fin n => ⟪a i, x⟫ = b i)).card = d)
    (hlong : ∀ w : ℕ → EuclideanSpace ℝ (Fin d),
      ¬ (w 0 = u ∧ w d = v ∧
        ∀ l < d, w l = w (l + 1) ∨ Adj (Hpoly a b) (w l) (w (l + 1)))) :
    ∃ η : ℝ, 0 < η ∧ ∀ ε : ℝ, 0 < ε → ε < η →
      ∀ w : ℕ → EuclideanSpace ℝ (Fin (d + 1)),
        ¬ (w 0 = toLp 2 (Fin.snoc (ofLp u) (0 : ℝ)) ∧
          w (d + 1) = toLp 2 (Fin.snoc (ofLp v) (0 : ℝ)) ∧
          ∀ l < d + 1, w l = w (l + 1) ∨
            Adj
              (Hpoly
                (Fin.snoc (fun i => toLp 2 (Fin.snoc (ofLp (a i))
                  (if i = k then (1 : ℝ) else if i = j then ε else 0)))
                  (toLp 2 (Fin.snoc (ofLp (a k)) (-1 : ℝ))))
                (Fin.snoc b (b k)))
              (w l) (w (l + 1))) := 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