Bounded clipped diameter is at most outer plus cut-face diameter plus one

Proved

Hirsch.bounded_clip_diameter_le_outer_add_cut_face_add_one

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

convex-geometrypolytopes

Let Q be an H-polyhedron in R^d, P=Q intersect {x:<c,x><=beta}, and F=Q intersect {x:<c,x>=beta}. If P is bounded, DiamLE Q B, and DiamLE F C, then DiamLE P (B+C+1). Q may be unbounded. No exterior outer vertex, nonempty clip, nonempty cut face, nonzero normal, or full-dimensionality assumption is required. This covers all clipped vertices, including newly created ones. It transfers two assumed bounds and does not prove the unrestricted polynomial Hirsch conjecture.

Preamble

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

Formal statement

theorem Hirsch.bounded_clip_diameter_le_outer_add_cut_face_add_one
    (d n B C : ℕ)
    (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)
    (hF : DiamLE (Hpoly a b ∩ {x | ⟪c, x⟫ = β}) C) :
    DiamLE (Hpoly a b ∩ {x | ⟪c, x⟫ ≤ β}) (B + C + 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