A vertex has trivial self common-face dimension

Proved

Hirsch.common_face_dim_of_vertex_self_eq_zero

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

convex-geometryhirsch-conjecturepolytopes

At a vertex the common-face dimension of the vertex with itself is zero.

Let $v$ be an extreme point of an H-polytope $P=\{x:\langle a_i,x\rangle\le b_i\}$ . The common-direction space of the pair $(v,v)$ is the kernel of all nonzero describing rows tight at $v$ . Those rows already span the dual, so the kernel is trivial and

\operatorname{dim} F(v,v)=0.

No boundedness or irredundancy hypothesis is used.

Formalization Note This is the $p=0$ (or $q=0$ ) special case of checkpoint localization when an endpoint is a vertex.

Preamble

import Definitions.Def_Hirsch_common_face_geometry

set_option autoImplicit false
open scoped RealInnerProductSpace
open Hirsch

Formal statement

namespace Hirsch

theorem common_face_dim_of_vertex_self_eq_zero
    {d n : ℕ}
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (v : EuclideanSpace ℝ (Fin d))
    (hv : v ∈ Set.extremePoints ℝ (Hpoly a b)) :
    HirschCommonFace.commonFaceDim a b v v = 0 := by sorry

end Hirsch

Source

Immediate from Prove2Me theorem Hirsch.vertex_tight_rows_span: the nonzero tight rows at an extreme point span, so their evaluation kernel is zero. Used as the p=q=0 case of Hirsch.common_face_checkpoint_localization.

View graph