Preparation and length increment: the missing step of Santos' strong $d$ -step for spindles

Proved

Hirsch.spindle_preparation_and_length

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$ , $n>2d$ rows, and no padded walk of length $d$ from $u$ to $v$ . Then there exist prepared data $a^0,b^0$ , apices $u^0,v^0$ and rows $k,j$ such that: all $b^0_i>0$ , the polytope is bounded, $u^0$ is feasible and $v^0$ is a vertex, the spindle (XOR) property holds, $k$ is tight at $v^0$ , $j$ is tight at $u^0$ , the rows tight at $u^0$ other than $j$ have trivial common kernel, and for every $\varepsilon_0>0$ there is $0<\varepsilon<\varepsilon_0$ such that the symmetric wedge over $k$ with row $j$ tilted by $\varepsilon$ admits no padded walk of length $d+1$ between $(u^0,0)$ and $(v^0,0)$ .

This is exactly the statement needed to finish Hirsch.spindle_one_step_axis: the remaining conjuncts (nonemptiness, boundedness, extremality of both lifted apices, XOR of the $n+1$ rows) are already proved for this construction. It follows from the row-simplicity preparation, the choice of a deletion-redundant row $j$ at the apex with more than $d$ tight rows (possible since $n>2d$ ), and the prepared-spindle length lemma.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

open scoped RealInnerProductSpace
open WithLp EuclideanSpace

Formal statement

namespace Hirsch

theorem spindle_preparation_and_length (d n : ℕ) (hd : 0 < d) (hn : 2 * d < n)
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : 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)
    (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)))) :
    ∃ (a0 : Fin n → EuclideanSpace ℝ (Fin d)) (b0 : Fin n → ℝ)
      (u0 v0 : EuclideanSpace ℝ (Fin d)) (k j : Fin n),
      (∀ i, 0 < b0 i) ∧ Bornology.IsBounded (Hpoly a0 b0) ∧
      u0 ∈ Hpoly a0 b0 ∧ v0 ∈ Set.extremePoints ℝ (Hpoly a0 b0) ∧
      (∀ i, (⟪a0 i, u0⟫ = b0 i) ↔ ⟪a0 i, v0⟫ ≠ b0 i) ∧
      ⟪a0 k, v0⟫ = b0 k ∧ ⟪a0 j, u0⟫ = b0 j ∧
      (∀ e : EuclideanSpace ℝ (Fin d),
        (∀ i, i ≠ j → ⟪a0 i, u0⟫ = b0 i → ⟪a0 i, e⟫ = 0) → e = 0) ∧
      ∀ ε0 : ℝ, 0 < ε0 → ∃ ε : ℝ, 0 < ε ∧ ε < ε0 ∧
        ∀ w : ℕ → EuclideanSpace ℝ (Fin (d + 1)),
          ¬ (w 0 = toLp 2 (Fin.snoc (ofLp u0) (0 : ℝ)) ∧
            w (d + 1) = toLp 2 (Fin.snoc (ofLp v0) (0 : ℝ)) ∧
            ∀ l < d + 1, w l = w (l + 1) ∨
              Adj
                (Hpoly
                  (Fin.snoc (fun i => toLp 2 (Fin.snoc (ofLp (a0 i))
                    (if i = k then (1 : ℝ) else if i = j then ε else 0)))
                    (toLp 2 (Fin.snoc (ofLp (a0 k)) (-1 : ℝ))))
                  (Fin.snoc b0 (b0 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

Preparation and length increment: the missing step of Santos' strong ddd-step for spindles

Preparation and length increment: the missing step of Santos' strong $d$ -step for spindles