A spindle can be pushed to be row-simple away from its apices

Proved

Hirsch.spindle_prepare_row_simple

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$ (every row tight at exactly one of them), $b_i>0$ , and no padded walk of length $d$ from $u$ to $v$ . Then there are normals $a^0$ with all right-hand sides $1$ such that $\mathrm{Hpoly}(a^0,\mathbf 1)$ is bounded, still a spindle with the same apices $u,v$ , every vertex other than $u,v$ has exactly $d$ tight rows, and there is still no padded walk of length $d$ from $u$ to $v$ .

This is the preprocessing Santos performs before the final perturbation in the proof of Theorem 2.6 ('if that is not the case, we first push $a$ to a generic point'). Rows tight at $u$ are pushed one at a time by convex combinations within the hyperplane $\{c:\langle c,u\rangle=1\}$ , likewise at $v$ ; each push is a graph contraction by the pushing lemma, so walk lower bounds are preserved, and a finite polynomial-avoidance argument makes every mixed $(d+1)$ -subset of augmented rows nonsingular, which forces row-simplicity away from the apices. Redundant rows are allowed throughout.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

open scoped RealInnerProductSpace
open WithLp EuclideanSpace

Formal statement

namespace Hirsch

theorem spindle_prepare_row_simple
    (d n : ℕ) (hd : 0 < d)
    (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),
      Bornology.IsBounded (Hpoly a0 (fun _ => 1)) ∧
      u ∈ Set.extremePoints ℝ (Hpoly a0 (fun _ => 1)) ∧
      v ∈ Set.extremePoints ℝ (Hpoly a0 (fun _ => 1)) ∧
      (∀ i, (⟪a0 i, u⟫ = 1) ↔ ⟪a0 i, v⟫ ≠ 1) ∧
      (∀ x ∈ Set.extremePoints ℝ (Hpoly a0 (fun _ => 1)),
        x ≠ u → x ≠ v →
        (Finset.univ.filter (fun i : Fin n => ⟪a0 i, x⟫ = 1)).card = d) ∧
      ∀ w : ℕ → EuclideanSpace ℝ (Fin d),
        ¬ (w 0 = u ∧ w d = v ∧
          ∀ l < d, w l = w (l + 1) ∨
            Adj (Hpoly a0 (fun _ => 1)) (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