Routing from face regions and surviving edges

Proved

Hirsch.route_of_faces_and_surviving_edges

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

graph-diameterhirsch-conjecturepath-repairpolyhedra

If every consecutive checkpoint pair is covered either by one certified extreme face or by one listed surviving parent edge, then a genuine parent walk has budget equal to the sum of all face diameter budgets plus the number of listed surviving edges.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

open scoped BigOperators RealInnerProductSpace
open Set Hirsch

Formal statement

theorem Hirsch.route_of_faces_and_surviving_edges
    {d : ℕ} {ι κ : Type*} [Fintype ι] [Fintype κ]
    (P : Set (EuclideanSpace ℝ (Fin d)))
    (F : ι → Set (EuclideanSpace ℝ (Fin d))) (B : ι → ℕ)
    (hF : ∀ i, IsExtreme ℝ P (F i)) (hD : ∀ i, DiamLE (F i) (B i))
    (a b : κ → EuclideanSpace ℝ (Fin d)) (hedge : ∀ e, Adj P (a e) (b e))
    (w : ℕ → EuclideanSpace ℝ (Fin d)) (L : ℕ)
    (hverts : ∀ k ≤ L, w k ∈ extremePoints ℝ P)
    (hcover : ∀ k < L,
      (∃ i, w k ∈ F i ∧ w (k + 1) ∈ F i) ∨
      (∃ e, w k ∈ ({a e, b e} : Set (EuclideanSpace ℝ (Fin d))) ∧
        w (k + 1) ∈ ({a e, b e} : Set (EuclideanSpace ℝ (Fin d))))) :
    ∃ q : ℕ → EuclideanSpace ℝ (Fin d),
      q 0 = w 0 ∧ q ((∑ i, B i) + Fintype.card κ) = w L ∧
      ∀ j < (∑ i, B i) + Fintype.card κ,
        q j = q (j + 1) ∨ Adj P (q j) (q (j + 1)) := by sorry

Source

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

View graph