Extreme-face repair networks route when every separating cut is bridged

Proved

Hirsch.extreme_face_cut_route_bound

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

graph-diameterhirsch-conjecturepolyhedrarepair-network

For a finite family of extreme faces with diameter budgets, if every partition separating the endpoint face labels has a genuine parent vertex shared across the cut, then the endpoint vertices admit a padded parent walk with budget equal to the sum of the face budgets.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

open scoped BigOperators RealInnerProductSpace
open Set Hirsch

Formal statement

namespace Hirsch

theorem extreme_face_cut_route_bound {d : ℕ} {ι : Type*} [Fintype ι]
    (P : Set (EuclideanSpace ℝ (Fin d)))
    (F : ι → Set (EuclideanSpace ℝ (Fin d))) (B : ι → ℕ)
    (hF : ∀ k, IsExtreme ℝ P (F k)) (hD : ∀ k, DiamLE (F k) (B k))
    (i j : ι)
    (hcut : ∀ A : Set ι, i ∈ A → j ∉ A →
      ∃ a ∈ A, ∃ b, b ∉ A ∧ ∃ z,
        z ∈ extremePoints ℝ P ∧ z ∈ F a ∧ z ∈ F b)
    (u v : EuclideanSpace ℝ (Fin d))
    (huP : u ∈ extremePoints ℝ P) (huF : u ∈ F i)
    (hvP : v ∈ extremePoints ℝ P) (hvF : v ∈ F j) :
    ∃ q : ℕ → EuclideanSpace ℝ (Fin d),
      q 0 = u ∧ q (∑ k, B k) = v ∧
      ∀ r < ∑ k, B k, q r = q (r + 1) ∨ Adj P (q r) (q (r + 1)) := by sorry

end Hirsch

Source

Verified Lean theorem from jjoshua2/prove2me-work PR #41.

View graph