Common-face dimensions overlap only through row excess

Proved

Hirsch.common_face_dimension_tradeoff

by jjosh · Sep 9, 2026 · Mathlib c5ea003 (Lean v4.30.0)

faceshirsch-conjecturelinear-algebrapolyhedra

For separated extreme endpoints u and v of an n-row H-polytope in dimension d, and any intermediate extreme vertex x, the dimensions of the common-direction spaces determined by (u,x) and (v,x) sum to at most d+(n-2d). In the balanced case n=2d they sum to at most d.

Preamble

import Definitions.Def_Hirsch_common_face_geometry

open scoped RealInnerProductSpace
open Set Hirsch

Formal statement

namespace Hirsch

theorem common_face_dimension_tradeoff
    {d n : ℕ}
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (u v x : EuclideanSpace ℝ (Fin d))
    (hu : u ∈ extremePoints ℝ (Hpoly a b))
    (hv : v ∈ extremePoints ℝ (Hpoly a b))
    (hx : x ∈ extremePoints ℝ (Hpoly a b))
    (hsep : ∀ i, a i ≠ 0 →
      ⟪a i, u⟫ ≠ b i ∨ ⟪a i, v⟫ ≠ b i) :
    HirschCommonFace.commonFaceDim a b u x +
      HirschCommonFace.commonFaceDim a b v x ≤ d + (n - 2 * d) := by sorry

end Hirsch

Source

Verified structural lemma from the Polynomial Hirsch formalization, jjoshua2/prove2me-work PR #30.

View graph