In the wedge of a prepared spindle, the only non-simple vertices on the tilted row are the two lifts of the apex

Proved

Hirsch.spindle_prepared_wedge_row_star

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

hirsch-conjecturepolytopessantos-counterexample

Let $P$ be a bounded spindle with apices $u,v$ , $b_i>0$ , row $k$ tight at $v$ , row $j$ tight at $u$ , and suppose every vertex of $P$ other than $u,v$ has exactly $d$ tight rows. Let $W$ be the symmetric wedge over row $k$ and $S=b_k-\langle a_k,u\rangle>0$ . Then $p=(u,-S)$ and $q=(u,S)$ are adjacent vertices of $W$ , row $j$ is tight at both, and every other vertex of $W$ on row $j$ has exactly $d+1$ tight rows.

This is the primal form of the genericity condition in the last paragraph of Santos' proof of Theorem 2.6 ('the only non-simplicial facets containing $a$ are $Q^+*u$ and $Q^+*w$ '). A vertex of $W$ on row $j$ projects to a vertex of $P$ on row $j$ , which is not $v$ ; if it is not $u$ it has $d$ tight rows, and exactly one roof (or, if $k$ is tight, both copies of $k$ replacing $k$ ) brings the count to $d+1$ .

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

open scoped RealInnerProductSpace
open WithLp EuclideanSpace

Formal statement

namespace Hirsch

theorem spindle_prepared_wedge_row_star
    (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)
    (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) :
    let A : Fin (n + 1) → EuclideanSpace ℝ (Fin (d + 1)) :=
      Fin.snoc (fun i => toLp 2 (Fin.snoc (ofLp (a i))
        (if i = k then (1 : ℝ) else 0)))
        (toLp 2 (Fin.snoc (ofLp (a k)) (-1 : ℝ)))
    let B : Fin (n + 1) → ℝ := Fin.snoc b (b k)
    let S : ℝ := b k - ⟪a k, u⟫
    let p : EuclideanSpace ℝ (Fin (d + 1)) := toLp 2 (Fin.snoc (ofLp u) (-S))
    let q : EuclideanSpace ℝ (Fin (d + 1)) := toLp 2 (Fin.snoc (ofLp u) S)
    0 < S ∧
    p ∈ Set.extremePoints ℝ (Hpoly A B) ∧
    q ∈ Set.extremePoints ℝ (Hpoly A B) ∧
    Adj (Hpoly A B) p q ∧
    ⟪A j.castSucc, p⟫ = B j.castSucc ∧
    ⟪A j.castSucc, q⟫ = B j.castSucc ∧
    ∀ x ∈ Set.extremePoints ℝ (Hpoly A B),
      ⟪A j.castSucc, x⟫ = B j.castSucc → x ≠ p → x ≠ q →
      (Finset.univ.filter (fun i : Fin (n + 1) => ⟪A i, x⟫ = B i)).card = d + 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