Extreme-face incidence cover bounds parent graph diameter

Proved

Hirsch.geodesic_face_cover_diameter_bound

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

extreme-facesgraph-diameterhirsch-conjecturepolyhedra

Let a connected vertex graph be covered by a finite family of extreme faces. If each vertex lies in at least q>0 selected faces and selected face i has intrinsic graph diameter at most B_i, then the parent padded diameter is at most (sum_i(B_i+1))/q - 1. The proof counts visits of a shortest path to faces and remains valid when the path leaves and later re-enters a face.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

open scoped RealInnerProductSpace BigOperators
open Set Hirsch
attribute [local instance] Classical.propDecidable

Formal statement

namespace Hirsch

theorem geodesic_face_cover_diameter_bound
    {ι : Type*} [Fintype ι]
    (d q : ℕ) (hq : 0 < q)
    (P : Set (EuclideanSpace ℝ (Fin d)))
    (F : ι → Set (EuclideanSpace ℝ (Fin d))) (B : ι → ℕ)
    (hF : ∀ i, IsExtreme ℝ P (F i))
    (hFD : ∀ i, DiamLE (F i) (B i))
    (hcover : ∀ x ∈ extremePoints ℝ P,
      q ≤ (Finset.univ.filter (fun i => x ∈ F i)).card)
    (hconnect : ∀ u ∈ extremePoints ℝ P, ∀ v ∈ extremePoints ℝ P,
      ∃ L : ℕ, ∃ w : ℕ → EuclideanSpace ℝ (Fin d),
        w 0 = u ∧ w L = v ∧
        ∀ j < L, w j = w (j + 1) ∨ Adj P (w j) (w (j + 1))) :
    DiamLE P ((∑ i, (B i + 1)) / q - 1) := by sorry

end Hirsch

Source

Verified graph-geometry theorem from the Polynomial Hirsch formalization, jjoshua2/prove2me-work PR #27.

View graph