Maximal row-circuit step common-face bound

Proved

Hirsch.maximal_row_circuit_step_common_face_bound

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

circuit-diameterformalizationgraph-diameterpolyhedra

Let an n-row H-polyhedron in ambient dimension d contain at least one extreme vertex z. For any maximal row-circuit step x→y, neither endpoint need be a vertex. If h is the coordinate dimension of the smallest common carrier of x and y and p is the coordinate dimension of the smallest face containing x, then h + d ≤ n + p. Thus maximality removes the destination-face correction term from the general nonvertex circuit-localization inequality.

Preamble

import Mathlib
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 maximal_row_circuit_step_common_face_bound
    {d n : ℕ}
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (z x y : EuclideanSpace ℝ (Fin d))
    (hz : z ∈ extremePoints ℝ (Hpoly a b))
    (hstep : RowCircuitStep a b x y) :
    HirschCommonFace.commonFaceDim a b x y + d ≤
      n + HirschCommonFace.commonFaceDim a b x x := by sorry
end Hirsch

Source

https://github.com/jjoshua2/prove2me-work/commit/2ef303016d5edbed0bb339fc7341b4f019ada400 ; independently compiled standalone from Actions run 34553646058.

View graph