Specified cut-face access with a possibly unbounded outer H-polyhedron

Proved

Hirsch.cut_face_access_of_unbounded_outer_diameter

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

convex-geometrypolytopes

Let Q be an H-polyhedron described by n inequalities in R^d and P=Q intersect {x:<c,x><=beta}. Assume P is bounded and the vertex-edge graph of Q has diameter at most B. For every two extreme points u,v of P with <c,v>=beta, some extreme point z of P on the SAME specified cut plane is reachable from u by at most B+1 edges. Q need not be bounded, and no outer extreme point on or beyond the cut plane is required. No nonzero-normal or full-dimensionality hypothesis is imposed. Larman is used only for connectivity of the bounded (n+1)-row clip; its numerical bound is discarded. This does not promise reaching v or establish a uniform polynomial outer-graph diameter bound.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model
open scoped RealInnerProductSpace
open Set Hirsch

Formal statement

theorem Hirsch.cut_face_access_of_unbounded_outer_diameter
    (d n B : ℕ)
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (c : EuclideanSpace ℝ (Fin d)) (β : ℝ)
    (hbd : Bornology.IsBounded (Hpoly a b ∩ {x | ⟪c, x⟫ ≤ β}))
    (hQ : DiamLE (Hpoly a b) B)
    (u v : EuclideanSpace ℝ (Fin d))
    (hu : u ∈ extremePoints ℝ (Hpoly a b ∩ {x | ⟪c, x⟫ ≤ β}))
    (hv : v ∈ extremePoints ℝ (Hpoly a b ∩ {x | ⟪c, x⟫ ≤ β}))
    (hvc : ⟪c, v⟫ = β) :
    ∃ z : EuclideanSpace ℝ (Fin d),
      z ∈ extremePoints ℝ (Hpoly a b ∩ {x | ⟪c, x⟫ ≤ β}) ∧
      ⟪c, z⟫ = β ∧
      ∃ w : ℕ → EuclideanSpace ℝ (Fin d),
        w 0 = u ∧ w (B + 1) = z ∧
        ∀ j < B + 1,
          w j = w (j + 1) ∨
            Adj (Hpoly a b ∩ {x | ⟪c, x⟫ ≤ β}) (w j) (w (j + 1)) := by sorry

Source

Working theorem for the Polynomial Hirsch mission; jjoshua2/prove2me-work, branch chatgpt/unbounded-cut-routing. No literature-priority claim.

View graph