Balanced row-circuit vertices must share a tight row

Proved

Hirsch.balanced_row_circuit_vertices_share_tight_row

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

balanced-polytopescircuitshirsch-conjectureobstructionpolyhedra

In an exactly balanced n=2d H-presentation with d at least two, two vertices whose displacement is a support-minimal row circuit must share a nonzero describing row that is tight at both endpoints. Thus an estranged balanced vertex pair cannot be a single row-circuit step.

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 balanced_row_circuit_vertices_share_tight_row
    {d n : ℕ}
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (u v : EuclideanSpace ℝ (Fin d))
    (hbal : n = 2 * d) (hd : 2 ≤ d)
    (hu : u ∈ extremePoints ℝ (Hpoly a b))
    (hv : v ∈ extremePoints ℝ (Hpoly a b))
    (hcirc : IsRowCircuit a (v - u)) :
    ∃ i : Fin n, a i ≠ 0 ∧ ⟪a i, u⟫ = b i ∧ ⟪a i, v⟫ = b i := 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