Common-face restriction never increases finite row-presentation excess
ProvedHirsch.common_face_has_subpresentation_faceDim_add_row_excessformalizationgraph-diameterpolyhedra
Let P={x in R^d : <a_i,x> <= b_i, i=1,...,n} be any finite H-presentation with d<=n. Let u be any feasible point and v any point. Form the common carrier by making every nonzero describing row that is tight at both u and v into an equality, and let h be its canonical coordinate dimension. Then the canonical coordinate H-polyhedron of that carrier has an equivalent subpresentation using original restricted rows and at most h+(n-d) inequalities. No boundedness, circuit, vertex, strict-feasibility, or irredundancy hypothesis is required.
Preamble
import Mathlib import Definitions.Def_Hirsch_common_face_geometry open scoped RealInnerProductSpace InnerProduct open Set Module Hirsch
Formal statement
namespace Hirsch
theorem common_face_has_subpresentation_faceDim_add_row_excess
{d n : ℕ}
(a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
(u v : EuclideanSpace ℝ (Fin d))
(hu : u ∈ Hpoly a b) (hdn : d ≤ n) :
HirschCommonFace.CommonFaceHasSubpresentationAtMost a b u v
(HirschCommonFace.commonFaceDim a b u v + (n - d)) := by sorry
end HirschSource