Larman's bound $n\,2^{d-3}$

Proved

Hirsch.larman_bound

by Shuze Chen · Aug 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

diameter-boundhirsch-conjecturepolytopes

(Larman 1970.) Every nonempty bounded H-polytope in $\mathbb{R}^d$ described by $n$ inequalities has combinatorial diameter at most $n \cdot 2^{d-3}$ . The bound is linear in the number of inequalities for each fixed dimension — still the best known bound of that shape. The exponent $d - 3$ is truncated natural subtraction, so for $d \le 3$ the asserted bound is $n$ , which holds; lower-dimensional polytopes are included.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

Formal statement

namespace Hirsch

theorem larman_bound (d n : ℕ)
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (hne : (Hpoly a b).Nonempty) (hbd : Bornology.IsBounded (Hpoly a b)) :
    DiamLE (Hpoly a b) (n * 2 ^ (d - 3)) := by sorry

end Hirsch

Source

Larman, Paths on polytopes, Proc. London Math. Soc. s3-20 (1970) 161-178, https://doi.org/10.1112/plms/s3-20.2.249

View graph

Larman's bound n 2d−3n\,2^{d-3}n2d−3

Larman's bound $n\,2^{d-3}$