Simultaneous clipping diameter bound for a pointed finite H-polyhedron

Proved

Hirsch.simultaneous_clip_diameter_from_pointed_finite_hpoly

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

clippingfar-capgraph-diameterhirsch-conjecturepointed-polyhedronpolyhedra

Let Q be a nonempty finite H-polyhedron in Euclidean space which contains no affine line. Suppose its old vertex-edge graph has padded diameter at most D. Intersect Q with finitely many additional linear halfspaces, and assume the final clipped set is compact. If the face where added inequality i is tight has intrinsic graph diameter at most B_i, then the final clipped polytope has padded graph diameter at most D + 1 + sum_i B_i. The proof derives the no-common-row-kernel characterization of pointedness, proves the old H-vertex set is finite, chooses a canonical summed-normal far cap internally, classifies every new cap vertex as a horizon vertex adjacent to an old vertex, and applies the verified strict-centre-free exterior clipping transfer.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

open scoped BigOperators RealInnerProductSpace
open Set Hirsch

Formal statement

namespace Hirsch

theorem simultaneous_clip_diameter_from_pointed_finite_hpoly
    {d n : ℕ} {ι : Type*} [Fintype ι]
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (hne : (Hpoly a b).Nonempty)
    (hpointed : ¬ ∃ x r : EuclideanSpace ℝ (Fin d),
      r ≠ 0 ∧ ∀ t : ℝ, x + t • r ∈ Hpoly a b)
    (f : ι → EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (c : ι → ℝ)
    (D : ℕ) (hD : DiamLE (Hpoly a b) D)
    (hPc : IsCompact (Hpoly a b ∩ {y | ∀ i, f i y ≤ c i}))
    (B : ι → ℕ)
    (hB : ∀ i, DiamLE
      ((Hpoly a b ∩ {y | ∀ j, f j y ≤ c j}) ∩ {x | f i x = c i}) (B i)) :
    DiamLE (Hpoly a b ∩ {y | ∀ i, f i y ≤ c i}) (D + 1 + ∑ i, B i) := by sorry

end Hirsch

Source

Kernel-verified pointed finite-H-polyhedron cap construction and clipping transfer in jjoshua2/prove2me-work.

View graph