Prove2Me

A relaxation keeping the tight rows of a vertex becomes bounded after one auxiliary cut

Proved
Hirsch.bounded_relaxation_cut

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

hirsch-conjecturelinear-programmingpolytopes

Let P={x∈Rd:⟨ai,x⟩≤bi, i<n}P=\{x\in\mathbb{R}^d:\langle a_i,x\rangle\le b_i,\ i<n\} be bounded, let TT be a set of row indices, and let vv be a vertex of PP all of whose tight inequalities have indices in TT. Put c=−∑j∈Tajc=-\sum_{j\in T}a_j. Then there is a real MM such that

⟨c,x⟩≤Mfor all x∈P,\langle c,x\rangle\le M\quad\text{for all }x\in P,

and the polyhedron

R={x∈Rd: ⟨aj,x⟩≤bj (j∈T),  ⟨c,x⟩≤M}R=\{x\in\mathbb{R}^d:\ \langle a_j,x\rangle\le b_j\ (j\in T),\ \ \langle c,x\rangle\le M\}

is bounded. Thus P⊆RP\subseteq R, and RR is a bounded H-polytope described by ∣T∣+1|T|+1 inequalities.

The relaxation {x:⟨aj,x⟩≤bj, j∈T}\{x:\langle a_j,x\rangle\le b_j,\ j\in T\} is in general unbounded; the single cut ⟨c,x⟩≤M\langle c,x\rangle\le M bounds it because a direction ee with ⟨aj,e⟩≤0\langle a_j,e\rangle\le0 for all j∈Tj\in T and −∑j∈T⟨aj,e⟩≤0-\sum_{j\in T}\langle a_j,e\rangle\le0 must satisfy ⟨aj,e⟩=0\langle a_j,e\rangle=0 for every j∈Tj\in T, and the normals indexed by TT span Rd\mathbb{R}^d since they contain the tight normals of the vertex vv. This is the device that lets a diameter induction apply its inductive hypothesis (stated for bounded polytopes) to Kalai--Kleitman or Larman relaxations.

Formalization Note The cut uses the specific normal −∑j∈Taj-\sum_{j\in T}a_j, as in the platform proof of Hirsch.graph_connected_general.

Preamble
import Mathlib
import Definitions.Def_Hirsch_model

open scoped RealInnerProductSpace
Formal statement
namespace Hirsch

theorem bounded_relaxation_cut (d n : ℕ)
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (hbd : Bornology.IsBounded (Hpoly a b)) (T : Finset (Fin n))
    (v : EuclideanSpace ℝ (Fin d)) (hv : v ∈ Set.extremePoints ℝ (Hpoly a b))
    (hvT : ∀ j, ⟪a j, v⟫ = b j → j ∈ T) :
    ∃ M : ℝ, (∀ x ∈ Hpoly a b, ⟪-∑ j ∈ T, a j, x⟫ ≤ M) ∧
      Bornology.IsBounded {x : EuclideanSpace ℝ (Fin d) |
        (∀ j ∈ T, ⟪a j, x⟫ ≤ b j) ∧ ⟪-∑ j ∈ T, a j, x⟫ ≤ M} := by sorry

end Hirsch
Source
Cut construction as in Prove2Me Hirsch.graph_connected_general (8b17b820-f7a3-42e4-89a3-efd89fad4f3b); recession-cone characterisation of boundedness: Bertsimas--Tsitsiklis, Introduction to Linear Optimization, Theorem 4.14 and Section 4.7 (a polyhedron is bounded iff its recession cone is {0}). G. Kalai, D. J. Kleitman, A quasi-polynomial bound for the diameter of graphs of polyhedra, Bull. AMS 26 (1992) 315-316, proof of the Lemma (the relaxed polyhedron cut out by the touched facets has no shorter paths), https://arxiv.org/abs/math/9204233; M. J. Todd, arXiv:1402.3579, Lemma 1.

View graph