Prove2Me

The cube blend is a bounded polytope with 2d+1−22^{d+1}-2 vertices

Proved
Hirsch.cube_blend_vertex_count

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

hirsch-conjecturepolytopes

For d≥2d\ge2 the polytope blendPoly d (the 3d3d inequalities dxi−s≤dd x_i-s\le d, −dxi+3s≤d2-dx_i+3s\le d^2, −dxi−s≤d2-dx_i-s\le d^2 with s=∑xis=\sum x_i) is nonempty and bounded, and its vertices are exactly the 2(2d−1)2(2^d-1) points

vσ(S):yi=−(d−k)/k (i∈S), yi=1 (i∉S),z=σ2(d−d−kk),v_\sigma(S):\quad y_i=-(d-k)/k\ (i\in S),\ y_i=1\ (i\notin S),\quad z=\tfrac{\sigma}{2}\bigl(d-\tfrac{d-k}{k}\bigr),

for ∅≠S⊆[d]\emptyset\ne S\subseteq[d], k=∣S∣k=|S|, σ=±1\sigma=\pm1, in the coordinates xi=yi+zx_i=y_i+z. Each is simple, with tight rows {Ui:i∉S}∪{Liσ:i∈S}\{U_i:i\notin S\}\cup\{L_i^\sigma:i\in S\}.

Proof idea. No vertex has z=0z=0; at z>0z>0 only upper and plus rows can be tight, at most one per index, so a vertex has exactly one tight row per index and not all upper; solving gives the displayed points, which are feasible with independent tight normals.

Preamble
import Mathlib
import Definitions.Def_Hirsch_model
import Definitions.Def_Hirsch_cube_blend

open scoped RealInnerProductSpace
Formal statement
namespace Hirsch

theorem cube_blend_vertex_count (d : ℕ) (hd : 2 ≤ d) :
    (blendPoly d).Nonempty ∧ Bornology.IsBounded (blendPoly d) ∧
    ∃ V : Finset (EuclideanSpace ℝ (Fin d)),
      (V : Set (EuclideanSpace ℝ (Fin d))) = Set.extremePoints ℝ (blendPoly d) ∧
      V.card = 2 ^ (d + 1) - 2 := by sorry

end Hirsch
Source
Campaign research notes (2026-09-06), Prove2Me mission 'The Polynomial Hirsch Conjecture', discussion thread; independently audited on-paper proofs, note 'deep_astra_geom' Sections 2.1-2.2 (audited with exact basis enumeration for d=3,4)

View graph