Facet access from ridge-visible access, by induction on dimension

Proved

Hirsch.access_of_ridge_visible_access

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

hirsch-conjecturepolytopes

Assume that for constants $C,k$ , in every bounded H-polytope with $n$ rows in $\mathbb R^d$ every vertex can reach, in $C(n+d)^k$ padded steps, a vertex that lies on a given nonzero row $i$ or on a nonzero row meeting row $i$ inside the polytope. Then in every such polytope every vertex can reach some vertex on row $i$ itself in $d\cdot C(n+d)^k$ padded steps.

Proof. Induction on $d$ . Reach a ridge-visible vertex $y$ in $C(n+d)^k$ steps; if $y$ is on row $i$ stop; otherwise apply the inductive hypothesis inside the facet through $y$ that meets row $i$ , which is a $(d-1)$ -polytope with $n-1$ rows (Hirsch.ridge_visible_access), and concatenate; walks are padded to the exact length.

With the platform's transfer theorem this shows that polynomial ridge-visible access implies the polynomial Hirsch conjecture with two more degrees.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model
import Definitions.Def_Hirsch_walk

open scoped RealInnerProductSpace

Formal statement

namespace Hirsch

theorem access_of_ridge_visible_access (C k : ℕ)
    (hrv : ∀ (d n : ℕ)
      (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ),
      Bornology.IsBounded (Hpoly a b) →
      ∀ u ∈ Set.extremePoints ℝ (Hpoly a b),
      ∀ i : Fin n, a i ≠ 0 →
      (∃ x ∈ Hpoly a b, ⟪a i, x⟫ = b i) →
      ∃ y ∈ Set.extremePoints ℝ (Hpoly a b),
        (⟪a i, y⟫ = b i ∨
          ∃ r : Fin n, r ≠ i ∧ a r ≠ 0 ∧ ⟪a r, y⟫ = b r ∧
            ∃ x ∈ Hpoly a b, ⟪a i, x⟫ = b i ∧ ⟪a r, x⟫ = b r) ∧
        Reach (Hpoly a b) (C * (n + d) ^ k) u y) :
    ∀ (d n : ℕ)
      (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ),
      Bornology.IsBounded (Hpoly a b) →
      ∀ u ∈ Set.extremePoints ℝ (Hpoly a b),
      ∀ i : Fin n, a i ≠ 0 →
      (∃ x ∈ Hpoly a b, ⟪a i, x⟫ = b i) →
      ∃ z ∈ Set.extremePoints ℝ (Hpoly a b), ⟪a i, z⟫ = b i ∧
        Reach (Hpoly a b) (d * (C * (n + d) ^ k)) u z := 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_grok' Section 4 (`access_dimension_step`)

View graph