Distance layers of a simple polytope form a connected layer family

Proved

Hirsch.distance_layers_clf

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

connected-layer-familieshirsch-conjecturepolytopes

Let $P=\{x:\langle a_i,x\rangle\le b_i,\ i<n\}\subseteq\mathbb R^d$ be bounded and simple (every vertex has exactly $d$ tight rows), and let $u,v$ be vertices. Layering the vertices by graph distance from $u$ , and identifying each vertex with the $d$ -set of its tight rows, produces a connected layer family of rank $d$ on the $n$ row indices whose length is $\mathrm{gdist}_P(u,v)$ and whose bases in layer $t$ are exactly the tight sets of the vertices at distance $t$ from $u$ .

This is Santos' Lemma 3.9 (the bridge between polytopes and the EHRR abstraction) in the mission's model. The interval axiom is the platform theorem Hirsch.tight_row_interval generalized from one row to an arbitrary set of rows: two vertices sharing a set $S$ of tight rows are joined, by Hirsch.face_connected, by a walk on which $S$ stays tight, and distances change by at most one per step. Distinctness of bases across layers is simplicity: a simple vertex is determined by its tight set.

Formalization Note The family's symbol type is Fin n; the conclusion identifies every base with the tight set of a vertex at the corresponding distance. Nonemptiness of intermediate layers uses a shortest walk (Hirsch.gdist_reach).

Preamble

import Mathlib
import Definitions.Def_Hirsch_model
import Definitions.Def_Hirsch_walk
import Definitions.Def_Hirsch_clf

open scoped RealInnerProductSpace

Formal statement

namespace Hirsch

theorem distance_layers_clf (d n : ℕ) (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (hbd : Bornology.IsBounded (Hpoly a b))
    (hsimple : ∀ x ∈ Set.extremePoints ℝ (Hpoly a b),
      (Finset.univ.filter (fun i : Fin n => ⟪a i, x⟫ = b i)).card = d)
    (u v : EuclideanSpace ℝ (Fin d))
    (hu : u ∈ Set.extremePoints ℝ (Hpoly a b)) (hv : v ∈ Set.extremePoints ℝ (Hpoly a b)) :
    ∃ F : CLF (Fin n) d, F.len = gdist (Hpoly a b) u v ∧
      ∀ t, ∀ B ∈ F.layer t, ∃ x ∈ Set.extremePoints ℝ (Hpoly a b),
        gdist (Hpoly a b) u x = t ∧ B = Finset.univ.filter (fun i => ⟪a i, x⟫ = b i) := by sorry

end Hirsch

Source

F. Santos, Recent progress on the combinatorial diameter of polytopes and simplicial complexes, TOP 21 (2013), arXiv:1307.5900, Section 3 (connected layer families, Definition 3.3, Lemma 3.9) Lemma 3.9; platform theorems Hirsch.tight_row_interval (da5f176c-7aef-4147-a763-5cd062e833ea), Hirsch.face_connected, Hirsch.gdist_reach

View graph