A vertex has at most row-excess many strictly slack inequalities
ProvedHirsch.vertex_strictly_slack_rows_card_le_row_excessformalizationgraph-diameterpolyhedra
Let P={x in R^d : <a_i,x> <= b_i} be any finite H-polyhedron described by n rows, and let v be a vertex. Then at most n-d describing inequalities are strictly slack at v. Equivalently, at least d describing rows are tight at every vertex. No boundedness, irredundancy, simplicity, or full-dimensionality assumption is required.
Preamble
import Mathlib import Definitions.Def_Hirsch_model open scoped RealInnerProductSpace open Set
Formal statement
namespace Hirsch
theorem vertex_strictly_slack_rows_card_le_row_excess
{d n : ℕ}
(a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
(v : EuclideanSpace ℝ (Fin d))
(hv : v ∈ Set.extremePoints ℝ (Hirsch.Hpoly a b)) :
(Finset.univ.filter (fun i => ⟪a i, v⟫ < b i)).card ≤ n - d := by sorry
end HirschSource