Prove2Me

Strong dd-step step with apices ±ed\pm e_d

Proved
Hirsch.spindle_one_step_axis

by jjosh · Sep 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

combinatorial-optimizationpolytope-theory

Santos' inductive step in standard position, with apices ±ed\pm e_d.

Let P⊆RdP\subseteq\mathbb R^d be a nonempty bounded H-polytope described by n>2dn>2d inequalities, with d>0d>0, whose apices are ede_d and −ed-e_d, forming a spindle of length greater than dd, and suppose inequality i0i_0 is tight at ede_d.

Then there is a nonempty bounded H-polytope P′⊆Rd+1P'\subseteq\mathbb R^{d+1} described by n+1n+1 inequalities which is a spindle of length greater than d+1d+1.

This is Theorem 2.6 of Santos written after the apices have been moved to ±ed\pm e_d: one-point-suspension of the polar prismatoid over the vertex dual to i0i_0, followed by the perturbation that makes the opposite base a facet.

Formalization Note. Apices are EuclideanSpace.single ⟨d-1, _⟩ (±1).

Preamble
import Mathlib
import Definitions.Def_Hirsch_model

open scoped RealInnerProductSpace
Formal statement
namespace Hirsch

/-- Santos' inductive step in standard position: apices $\pm e_d$, facet through
the positive apex.

If $P\subseteq\mathbb R^d$ is a $d$-spindle of length greater than $d$ with
apices $e_d$ and $-e_d$, $n>2d$ inequalities, and inequality $i_0$ tight at
$e_d$, then there is a $(d+1)$-spindle with $n+1$ inequalities and length
greater than $d+1$. -/
theorem spindle_one_step_axis (d n : ℕ) (hd : 0 < d) (hn : 2 * d < n)
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (i0 : Fin n)
    (hne : (Hpoly a b).Nonempty) (hbd : Bornology.IsBounded (Hpoly a b))
    (hu : EuclideanSpace.single ⟨d - 1, Nat.sub_lt hd (by decide)⟩ (1 : ℝ) ∈
      Set.extremePoints ℝ (Hpoly a b))
    (hv : EuclideanSpace.single ⟨d - 1, Nat.sub_lt hd (by decide)⟩ (-1 : ℝ) ∈
      Set.extremePoints ℝ (Hpoly a b))
    (hspindle : ∀ i,
      (⟪a i, EuclideanSpace.single ⟨d - 1, Nat.sub_lt hd (by decide)⟩ (1 : ℝ)⟫ = b i) ↔
        ⟪a i, EuclideanSpace.single ⟨d - 1, Nat.sub_lt hd (by decide)⟩ (-1 : ℝ)⟫ ≠ b i)
    (htight : ⟪a i0, EuclideanSpace.single ⟨d - 1, Nat.sub_lt hd (by decide)⟩ (1 : ℝ)⟫ = b i0)
    (hlong : ∀ w : ℕ → EuclideanSpace ℝ (Fin d),
      ¬ (w 0 = EuclideanSpace.single ⟨d - 1, Nat.sub_lt hd (by decide)⟩ (1 : ℝ) ∧
          w d = EuclideanSpace.single ⟨d - 1, Nat.sub_lt hd (by decide)⟩ (-1 : ℝ) ∧
          ∀ j < d, w j = w (j + 1) ∨ Adj (Hpoly a b) (w j) (w (j + 1)))) :
    ∃ (a' : Fin (n + 1) → EuclideanSpace ℝ (Fin (d + 1)))
      (b' : Fin (n + 1) → ℝ)
      (u' v' : EuclideanSpace ℝ (Fin (d + 1))),
      (Hpoly a' b').Nonempty ∧
      Bornology.IsBounded (Hpoly a' b') ∧
      u' ∈ Set.extremePoints ℝ (Hpoly a' b') ∧
      v' ∈ Set.extremePoints ℝ (Hpoly a' b') ∧
      (∀ i, (⟪a' i, u'⟫ = b' i) ↔ ⟪a' i, v'⟫ ≠ b' i) ∧
      ∀ w : ℕ → EuclideanSpace ℝ (Fin (d + 1)),
        ¬ (w 0 = u' ∧ w (d + 1) = v' ∧
            ∀ j < d + 1, w j = w (j + 1) ∨
              Adj (Hpoly a' b') (w j) (w (j + 1))) := by sorry

end Hirsch
Source
F. Santos, A counterexample to the Hirsch conjecture, Ann. of Math. 176 (2012) 383-412, https://arxiv.org/abs/1006.2814, Theorem 2.6 (inductive step in Section 2.2).

View graph