Connected layer families (EHRR abstraction of polytope graphs)

Definition

Hirsch_clf

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

combinatoricsconnected-layer-familieshirsch-conjecture

The combinatorial abstraction of polytope graphs introduced by Eisenbrand, Hähnle, Razborov and Rothvoß and used throughout Santos' survey (Section 3).

A connected layer family (CLF) of rank $d$ on a finite symbol set $V$ is a finite sequence of nonempty layers $\mathcal L_0,\dots,\mathcal L_L$ of $d$ -subsets of $V$ (bases) such that no base occurs in two layers and, for every $S\subseteq V$ , the set of layer indices whose layer contains a base $\supseteq S$ is an interval. Its length is $L$ . Layering the vertices of a simple $d$ -polytope with $n$ facets by graph distance from a fixed vertex, and identifying each vertex with its set of $d$ tight facets, gives a CLF on $n$ symbols whose length is the eccentricity of that vertex (Santos, Lemma 3.9). Hence upper bounds on the length of CLFs bound polytope diameters; the Kalai--Kleitman and Larman arguments go through verbatim in this abstraction, while EHRR exhibit CLFs of length $\Omega(n^2/\log n)$ .

The file provides the structure CLF V d, the profile of a base with respect to a block assignment $\mathrm{blk}:V\to G$ , the class of saturated homogeneous families (every layer has a single profile $p$ and contains a base above every subset of size $<d$ compatible with $p$ ; this class contains the EHRR mesh constructions), and the ridge-incidence condition that every $(d-1)$ -subset lies in at most $\rho$ bases of the family.

Formalization Note Layers are indexed by Fin (len + 1); the interval axiom is stated as betweenness for three indices. The abstraction is purely combinatorial and does not import the polytope model.

Definition code

import Mathlib

/-!
# Connected layer families

The combinatorial abstraction of polytope graphs used by Eisenbrand, Hähnle, Razborov
and Rothvoß (*Diameter of polyhedra: limits of abstraction*, Math. Oper. Res. 35 (2010))
and by Santos (*Recent progress on the combinatorial diameter of polytopes and simplicial
complexes*, TOP 21 (2013), §3).

A **connected layer family** (CLF) of rank `d` on a finite symbol type `V` is a finite
sequence of nonempty layers `L 0, …, L (len)` of `d`-subsets of `V` ("bases"), such that
no base appears in two layers, and for every subset `S ⊆ V` the set of layer indices
whose layer contains a base ⊇ `S` is an interval.  The layers of a polytope by graph
distance from a vertex form such a family (Santos, Lemma 3.9), so upper bounds on the
length of CLFs are upper bounds on polytope diameters.

Several finer classes are used in the campaign notes:
* `IsSaturatedHomogeneous`: with respect to a fixed partition of `V` into blocks
  (given by `blk : V → G`), every layer has all its bases of one *profile*
  (numbers of symbols per block), and contains a base above every subset of
  cardinality `< d` that is compatible with that profile.  This class contains the
  EHRR mesh constructions.
* `RidgeIncidenceLE ρ`: every `(d-1)`-subset is contained in at most `ρ` bases
  of the family (the polytopal case has `ρ = 2` for simple polytopes).
-/

namespace Hirsch

/-- A connected layer family of rank `d` with layers indexed by `Fin (len + 1)`. -/
structure CLF (V : Type*) [DecidableEq V] [Fintype V] (d : ℕ) where
  /-- The number of layers minus one (the *length* of the family). -/
  len : ℕ
  /-- The layers. -/
  layer : Fin (len + 1) → Finset (Finset V)
  /-- Every layer is nonempty. -/
  nonempty : ∀ t, (layer t).Nonempty
  /-- Every member of a layer is a base: a `d`-subset of `V`. -/
  card_eq : ∀ t, ∀ B ∈ layer t, B.card = d
  /-- No base appears in two different layers. -/
  disjoint : ∀ t t', t ≠ t' → Disjoint (layer t) (layer t')
  /-- The connectivity axiom: for every `S`, the layers containing a base above `S`
  form an interval of indices. -/
  interval : ∀ (S : Finset V) (t₁ t₂ t₃ : Fin (len + 1)), t₁ ≤ t₂ → t₂ ≤ t₃ →
    (∃ B ∈ layer t₁, S ⊆ B) → (∃ B ∈ layer t₃, S ⊆ B) → ∃ B ∈ layer t₂, S ⊆ B

namespace CLF

variable {V : Type*} [DecidableEq V] [Fintype V] {d : ℕ}

/-- The profile of a base with respect to a block assignment `blk`: the number of its
symbols in each block. -/
def profile {G : Type*} [DecidableEq G] (blk : V → G) (B : Finset V) : G → ℕ :=
  fun g => (B.filter (fun x => blk x = g)).card

/-- A layer family is *saturated homogeneous* with respect to `blk` if each layer has a
single profile `p`, and every subset `S` with `S.card < d` whose profile is pointwise
`≤ p` is contained in some base of that layer. -/
def IsSaturatedHomogeneous {G : Type*} [DecidableEq G] [Fintype G]
    (blk : V → G) (F : CLF V d) : Prop :=
  ∀ t, ∃ p : G → ℕ,
    (∀ B ∈ F.layer t, profile blk B = p) ∧
    (∀ S : Finset V, S.card < d → (∀ g, profile blk S g ≤ p g) →
      ∃ B ∈ F.layer t, S ⊆ B)

/-- Every `(d-1)`-subset of `V` lies in at most `ρ` bases of the whole family. -/
def RidgeIncidenceLE (F : CLF V d) (ρ : ℕ) : Prop :=
  ∀ R : Finset V, R.card = d - 1 →
    ((Finset.univ : Finset (Fin (F.len + 1))).biUnion
      (fun t => (F.layer t).filter (fun B => R ⊆ B))).card ≤ ρ

end CLF

end Hirsch

Source

F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Diameter of polyhedra: limits of abstraction, Math. Oper. Res. 35 (2010) 786-794, https://doi.org/10.1287/moor.1100.0470; 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)

View graph