Polynomial target-face access implies a polynomial diameter bound

Proved

Hirsch.diameter_bound_of_target_face_access

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

graph-diameterhirsch-conjecturepolyhedrapolytopes

Fix natural numbers $C,k$ . For each bounded H-polytope $P\subseteq\mathbb R^d$ described by $n$ inequalities, suppose the following access property holds. Whenever distinct vertices $u,v$ share no tight inequality with nonzero normal, there exist a vertex $z$ and a row $i$ such that

a_i\ne0,\qquad \langle a_i,v\rangle=\langle a_i,z\rangle=b_i,

and a walk from $u$ to $z$ of at most $C(n+d)^k$ edge crossings. The estimate and its constants must hold uniformly for all dimensions, descriptions, and such endpoint pairs.

Then every bounded H-polytope with $n$ rows in ambient dimension $d$ satisfies

\operatorname{DiamLE}\bigl(P,dC(n+d)^k\bigr).

This is a conditional local-to-global theorem: it turns a uniform target-face access estimate into a diameter estimate, losing one polynomial degree. It supplies neither the access estimate nor universal constants. The result applies to redundant descriptions and lower-dimensional polytopes, with no simplicity assumption.

Formalization Note The access and diameter walks allow stationary steps, so their budgets are written as exact natural-number lengths. Nonemptiness is not a separate hypothesis: empty polytopes have no extreme-point pairs. The supporting row is required to have nonzero normal but need not be facet-defining.

Preamble

import Definitions.Def_Hirsch_model

open scoped RealInnerProductSpace

Formal statement

namespace Hirsch

theorem diameter_bound_of_target_face_access (C k : ℕ)
    (haccess : ∀ (d n : ℕ)
      (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ),
      Bornology.IsBounded (Hpoly a b) →
      ∀ u ∈ Set.extremePoints ℝ (Hpoly a b),
      ∀ v ∈ Set.extremePoints ℝ (Hpoly a b), u ≠ v →
      (∀ i, a i ≠ 0 → ⟪a i, u⟫ ≠ b i ∨ ⟪a i, v⟫ ≠ b i) →
      ∃ (i : Fin n) (z : EuclideanSpace ℝ (Fin d)),
        a i ≠ 0 ∧ ⟪a i, v⟫ = b i ∧
        z ∈ Set.extremePoints ℝ (Hpoly a b) ∧ ⟪a i, z⟫ = b i ∧
        ∃ w : ℕ → EuclideanSpace ℝ (Fin d),
          w 0 = u ∧ w (C * (n + d) ^ k) = z ∧
          ∀ j < C * (n + d) ^ k,
            w j = w (j + 1) ∨ Adj (Hpoly a b) (w j) (w (j + 1))) :
    ∀ (d n : ℕ) (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ),
      Bornology.IsBounded (Hpoly a b) → DiamLE (Hpoly a b) (d * C * (n + d) ^ k) := by sorry

end Hirsch

Source

Original conditional dimension-induction reduction of the polynomial Hirsch conjecture. Context: F. Santos, Recent progress on the combinatorial diameter of polytopes and simplicial complexes, TOP 21 (2013), arXiv:1307.5900, Conjecture 1.1 (pp. 1–2), https://arxiv.org/abs/1307.5900. Geometric ingredient: Prove2Me Hirsch.facet_reduction, theorem 11b3500a-b9f8-4b44-94aa-d71354441ddb. This conditional statement is derived here, not attributed as a theorem of Santos.

View graph