Dimension drop for facet access from a ridge-visible vertex

Proved

Hirsch.ridge_visible_access

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

hirsch-conjecturepolytopes

Let $P\subseteq\mathbb R^d$ be a bounded H-polytope with $k+1$ rows, $u$ a vertex, and $i\ne r$ two rows with nonzero normals such that $r$ is tight at $u$ and rows $i$ and $r$ meet inside $P$ (the facet through $u$ sees the target face across a ridge). If every bounded H-polytope in $\mathbb R^{d-1}$ with $k$ rows has facet access at most $B$ , then some vertex of $P$ on row $i$ is reachable from $u$ by a padded walk of length $B$ .

Proof idea. Chart the face of row $r$ as a $(d-1)$ -polytope with $k$ rows (the platform's Hirsch.facet_walk); row $i$ restricted to it is a nonempty face; apply the hypothesis there and push the walk back into $P$ , where it stays on the face of row $r$ .

Together with Hirsch.access_of_ridge_visible_access, this reduces polynomial facet access to reaching a ridge-visible vertex in polynomially many steps.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model
import Definitions.Def_Hirsch_walk

open scoped RealInnerProductSpace

Formal statement

namespace Hirsch

theorem ridge_visible_access (d k : ℕ)
    (a : Fin (k + 1) → EuclideanSpace ℝ (Fin d)) (b : Fin (k + 1) → ℝ)
    (hbd : Bornology.IsBounded (Hpoly a b))
    (u : EuclideanSpace ℝ (Fin d)) (hu : u ∈ Set.extremePoints ℝ (Hpoly a b))
    (i r : Fin (k + 1)) (hir : i ≠ r) (hai : a i ≠ 0) (har : a r ≠ 0)
    (hru : ⟪a r, u⟫ = b r)
    (hridge : ∃ x ∈ Hpoly a b, ⟪a i, x⟫ = b i ∧ ⟪a r, x⟫ = b r)
    (B : ℕ)
    (IH : ∀ (a' : Fin k → EuclideanSpace ℝ (Fin (d - 1))) (b' : Fin k → ℝ),
      Bornology.IsBounded (Hpoly a' b') →
      ∀ u' ∈ Set.extremePoints ℝ (Hpoly a' b'),
      ∀ i' : Fin k, 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') B u' z') :
    ∃ z ∈ Set.extremePoints ℝ (Hpoly a b), ⟪a i, z⟫ = b i ∧
      Reach (Hpoly a b) B 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' Lemma 2.5; platform theorem Hirsch.facet_walk (c2ce1a4d-7f43-423d-9408-57eb09cc552a)

View graph