Given-facet access is polynomial iff the polynomial Hirsch conjecture holds

Proved

Hirsch.given_face_access_iff_polynomial_hirsch

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

hirsch-conjectureopen-problempolytopes

The following two existence statements are equivalent:

there are $C,k$ such that in every bounded H-polytope, for vertices $u\ne v$ sharing no tight nonzero row and every nonzero row $i$ tight at $v$ , some vertex on row $i$ is reachable from $u$ by a padded walk of length $C(n+d)^k$ (the mission leaf polynomial_access_to_given_supporting_face);
there are $c,k$ such that every nonempty bounded H-polytope has diameter at most $c(n+d)^k$ (the mission's root, polynomial_hirsch_conjecture).

Direction 2 ⇒ 1 walks to $v$ itself. Direction 1 ⇒ 2 is the truncation reduction: for vertices $u\ne v$ , cut off $v$ by one extra row exposing it; the new row is tight at every new vertex and slack at $u$ , no nonzero row is tight at $u$ and at a new vertex, and access to the new row in the truncation equals the distance from $u$ to $v$ in $P$ ; the extra row costs at most one in $n$ , absorbed by the constants. This records precisely that the platform's given-facet leaf is not weaker than the conjecture itself.

Formalization Note Both sides are stated verbatim as on the platform. The equivalence loses at most a constant factor and no degree.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

open scoped RealInnerProductSpace

Formal statement

namespace Hirsch

theorem given_face_access_iff_polynomial_hirsch :
    (∃ 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 →
      (∀ j, a j ≠ 0 → ⟪a j, u⟫ ≠ b j ∨ ⟪a j, v⟫ ≠ b j) →
      ∀ i : Fin n, a i ≠ 0 → ⟪a i, v⟫ = b i →
      ∃ z : EuclideanSpace ℝ (Fin d),
        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))) ↔
    (∃ c k : ℕ, ∀ (d n : ℕ) (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ),
      (Hpoly a b).Nonempty → Bornology.IsBounded (Hpoly a b) →
      DiamLE (Hpoly a b) (c * (n + d) ^ k)) := 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 'access_astra' Lemma 1.3 / Section 2.3 and 'access_astra_disproof' Section 1.4 (audited); transfer theorem Hirsch.diameter_bound_of_target_face_access (73f50dd9-2186-4d19-93f8-7c0b62bf876b)

View graph