Row-circuit endpoints lie in a small common face

Proved

Hirsch.row_circuit_common_face_dimension_bound

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

circuitscommon-facesdimensionhirsch-conjecturepolyhedra

Let u and v be vertices of an n-row H-polytope in ambient dimension d. If the displacement v-u is a support-minimal row circuit, then the face cut out by all nonzero describing rows tight at both endpoints has dimension h satisfying 2h+d <= n+1 (equivalently 2h <= n-d+1). No simplicity, irredundancy, strict-feasibility, or maximal-step assumption is required.

Preamble

import Definitions.Def_Hirsch_common_face_geometry
import Definitions.Def_Hirsch_circuit_slack_model

open scoped RealInnerProductSpace
open Set Hirsch

Formal statement

namespace Hirsch

theorem row_circuit_common_face_dimension_bound
    {d n : ℕ}
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (u v : EuclideanSpace ℝ (Fin d))
    (hu : u ∈ extremePoints ℝ (Hpoly a b))
    (hv : v ∈ extremePoints ℝ (Hpoly a b))
    (hcirc : IsRowCircuit a (v - u)) :
    2 * HirschCommonFace.commonFaceDim a b u v + d ≤ n + 1 := by sorry

end Hirsch

Source

Kernel- and standalone-verified proof from jjoshua2/prove2me-work commit 9f964b8617fbbcae3cf652c130cbdbacd32b0dea, Actions run 34495410594. Related circuit-diameter literature is background only; no novelty claim is made.

View graph