Polynomial access to a supporting face of the target vertex (conjectural)

Open

Hirsch.polynomial_target_face_access

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

graph-diameterhirsch-conjecturepolyhedrapolytopes

Is there a polynomial budget for reaching a supporting face containing a target vertex, without requiring that the target vertex itself be reached?

Precisely, there exist natural numbers $C,k$ , independent of all data, with the following property. Let

P=\{x\in\mathbb R^d:\langle a_i,x\rangle\le b_i\ (i=1,\ldots,n)\}

be bounded, and let $u\ne v$ be extreme points of $P$ . Suppose no row with nonzero normal is tight at both endpoints: for every $i$ with $a_i\ne0$ , at least one of

\langle a_i,u\rangle\ne b_i,\qquad \langle a_i,v\rangle\ne b_i

holds. Then there are a row $i$ , an extreme point $z$ of $P$ , and a vertex-edge walk from $u$ to $z$ such that

a_i\ne0,\qquad \langle a_i,z\rangle=\langle a_i,v\rangle=b_i, \qquad \operatorname{length}(u\leadsto z)\le C(n+d)^k.

Only access to one nonzero supporting row of the target is required; $z$ need not equal $v$ , and the walk need not be monotone or non-revisiting. This is an explicitly conjectural local-routing subproblem for the polynomial Hirsch conjecture, not a known polynomial estimate. The conditional theorem Hirsch.diameter_bound_of_target_face_access gives its role in the decomposition: uniform access bounds imply diameter bounds with one additional polynomial degree. No values of $C,k$ are claimed here.

Formalization Note Ambient dimension and row count may be zero; distinct extreme points exclude the zero-dimensional case. Redundant rows, zero normals, and lower-dimensional polytopes are allowed. A row with zero normal cannot satisfy the conclusion. The supporting section need not be a facet. Walks allow stationary steps and are represented with exactly $C(n+d)^k$ steps.

Preamble

import Definitions.Def_Hirsch_model

open scoped RealInnerProductSpace

Formal statement

namespace Hirsch

theorem polynomial_target_face_access :
    ∃ C k : ℕ, ∀ (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)) := by sorry

end Hirsch

Source

Original conjectural target-face-access subproblem, derived for Prove2Me Hirsch.balanced_polynomial_bound (cdb2b059-17b6-4c73-8740-caca090314d7) through Hirsch.diameter_bound_of_target_face_access. Context: F. Santos, Recent progress on the combinatorial diameter of polytopes and simplicial complexes, TOP 21 (2013), arXiv:1307.5900, p. 2, Conjecture 1.1, https://arxiv.org/abs/1307.5900. This local formulation is proposed here and is NOT attributed as an established theorem or an exact quoted conjecture from Santos.

View graph