Polynomial Hirsch bound for balanced H-polytopes

Open

Hirsch.balanced_polynomial_bound

by Yuning · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricshirsch-conjecturepolyhedrapolytopes

There exist constants $C,k\in\mathbb{N}$ such that every nonempty bounded H-polytope $Q\subseteq\mathbb{R}^D$ described by exactly $2D$ linear inequalities has combinatorial diameter at most $C D^k$ :

\operatorname{DiamLE}(Q,\, C\, D^k).

This is the polynomial Hirsch conjecture restricted to balanced descriptions. Via the description-level balancing transfer (padding tautological inequalities or iterating a Klee–Walkup wedge), the two existence statements are equivalent: the unrestricted conjecture with constants $c,k$ implies this balanced form with constants $C=c\cdot 3^k$ and the same exponent $k$ . The balanced bound remains conjectural.

Formalization Note The statement quantifies over every ambient dimension $D$ , including $D=0$ . Natural-number exponentiation uses the convention $0^0=1$ .

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

open scoped RealInnerProductSpace

Formal statement

namespace Hirsch

theorem balanced_polynomial_bound :
    ∃ C k : ℕ, ∀ (D : ℕ) (a : Fin (2 * D) → EuclideanSpace ℝ (Fin D)) (b : Fin (2 * D) → ℝ),
      (Hpoly a b).Nonempty → Bornology.IsBounded (Hpoly a b) →
      DiamLE (Hpoly a b) (C * D ^ k) := by sorry

end Hirsch

Source

The polynomial Hirsch conjecture restricted to descriptions with n = 2d inequalities. Kalai, The polynomial Hirsch conjecture (Polymath 3), 2010, https://gilkalai.wordpress.com/2010/09/29/the-polynomial-hirsch-conjecture-a-proposal-for-polymath3/; Santos, TOP 21 (2013), arXiv:1307.5900. Equivalent to the unrestricted conjecture after the balancing transfer.

View graph