Truncating a vertex turns vertex distance into facet access

Proved

Hirsch.truncation_access_eq_dist

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

hirsch-conjecturepolytopes

Let $P$ be a bounded H-polytope with $n$ rows and $u\ne v$ two vertices. There is a nonzero normal $c$ and a level $\gamma$ with $\langle c,x\rangle<\gamma<\langle c,v\rangle$ for every vertex $x\ne v$ , such that in the truncated polytope $Q=P\cap\{\langle c,x\rangle\le\gamma\}$ , described by $n+1$ rows, $u$ is still a vertex and for every $L$ ,

\text{some vertex } z \text{ of } Q \text{ on the new row is reached from } u \text{ by a padded walk of length } L\iff v \text{ is reached from } u \text{ in } P \text{ by a padded walk of length } L .

So access to a genuine facet is exactly as hard as vertex-to-vertex distance: a polynomial bound on given-facet access (even to a facet that is a simplex, when $P$ is simple) implies a polynomial bound on the diameter with the same constants, and conversely. In particular the mission leaves polynomial_access_to_given_supporting_face, polynomial_target_face_access and polynomial_hirsch_conjecture are equivalent as polynomial existence statements.

Proof idea. Only $v$ is cut off; the new vertices are the points of the cut on the old edges at $v$ , all other vertices and the edges not at $v$ survive, and edges at $v$ are shortened. A walk to $v$ is rerouted to the cut point on its last edge, and a walk to the cut is stopped at its first arrival.

Formalization Note c is the sum of the normals tight at v (which exposes v), and γ separates the finitely many vertex values.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model
import Definitions.Def_Hirsch_walk

open scoped RealInnerProductSpace

Formal statement

namespace Hirsch

theorem truncation_access_eq_dist (d n : ℕ) (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (hbd : Bornology.IsBounded (Hpoly a b))
    (u v : EuclideanSpace ℝ (Fin d))
    (hu : u ∈ Set.extremePoints ℝ (Hpoly a b)) (hv : v ∈ Set.extremePoints ℝ (Hpoly a b))
    (huv : u ≠ v) :
    ∃ (c : EuclideanSpace ℝ (Fin d)) (γ : ℝ),
      c ≠ 0 ∧ γ < ⟪c, v⟫ ∧ ⟪c, u⟫ < γ ∧
      (∀ x ∈ Set.extremePoints ℝ (Hpoly a b), x ≠ v → ⟪c, x⟫ < γ) ∧
      let a' : Fin (n + 1) → EuclideanSpace ℝ (Fin d) := Fin.snoc a c
      let b' : Fin (n + 1) → ℝ := Fin.snoc b γ
      u ∈ Set.extremePoints ℝ (Hpoly a' b') ∧
      (∀ L : ℕ, (∃ z ∈ Set.extremePoints ℝ (Hpoly a' b'), ⟪c, z⟫ = γ ∧ Reach (Hpoly a' b') L u z) ↔
        Reach (Hpoly a b) L u v) := 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' Section 2.3 (audited); exposing normal: platform theorem Hirsch.vertex_exposing_redundant_row_extension

View graph