Prove2Me

Strong dd-step step from a chosen apex facet

Proved
Hirsch.spindle_one_step_from_apex_facet

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

combinatorial-optimizationpolytope-theory

Santos' inductive step, starting from a chosen facet through one apex.

Let P⊆RdP\subseteq\mathbb R^d be a nonempty bounded H-polytope described by nn inequalities, with 0<d0<d and n>2dn>2d. Suppose u,vu,v are extreme points forming a spindle of length greater than dd, and inequality i0i_0 is tight at uu.

Then there exist a nonempty bounded H-polytope P′⊆Rd+1P'\subseteq\mathbb R^{d+1} described by n+1n+1 inequalities, together with extreme points u′,v′u',v' of P′P', such that P′P' is a spindle with apices u′,v′u',v' and there is no padded vertex-edge walk of length d+1d+1 from u′u' to v′v'.

This is the polar of the one-point-suspension-plus-perturbation in Santos, Theorem 2.6: one first wedges over the facet through uu corresponding to i0i_0, then perturbs so that the image of the opposite base becomes a facet, increasing the spindle length by one.

Formalization Note. The facet through uu is passed as an index i0i_0 with ⟨ai0,u⟩=bi0\langle a_{i_0},u\rangle=b_{i_0}.

Preamble
import Mathlib
import Definitions.Def_Hirsch_model

open scoped RealInnerProductSpace
Formal statement
namespace Hirsch

/-- Santos' inductive step, starting from a chosen facet through one apex.

If $P\subseteq\mathbb R^d$ is a $d$-spindle of length greater than $d$ with
$n>2d$ inequalities, and inequality $i_0$ is tight at the apex $u$, then
the one-point-suspension-plus-perturbation of Santos (Theorem 2.6, polarised)
produces a $(d+1)$-spindle with $n+1$ inequalities and length greater than
$d+1$. -/
theorem spindle_one_step_from_apex_facet (d n : ℕ) (hd : 0 < d) (hn : 2 * d < n)
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (u v : EuclideanSpace ℝ (Fin d)) (i0 : Fin n)
    (hne : (Hpoly a b).Nonempty) (hbd : Bornology.IsBounded (Hpoly a b))
    (hu : u ∈ Set.extremePoints ℝ (Hpoly a b))
    (hv : v ∈ Set.extremePoints ℝ (Hpoly a b))
    (hspindle : ∀ i, (⟪a i, u⟫ = b i) ↔ ⟪a i, v⟫ ≠ b i)
    (htight : ⟪a i0, u⟫ = b i0)
    (hlong : ∀ w : ℕ → EuclideanSpace ℝ (Fin d),
      ¬ (w 0 = u ∧ w d = v ∧
          ∀ 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 1.5 and Theorem 2.6 (inductive step, Section 2.2).

View graph