Connected layer families with one base per layer have length at most $n-d$

Proved

Hirsch.clf_singleton_layers_linear

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

combinatoricsconnected-layer-familieshirsch-conjecture

If every layer of a connected layer family of rank $d\ge1$ on $n$ symbols consists of a single base, then its length satisfies $L\le n-d$ .

Every symbol has an interval lifetime; at each transition some element enters the new base, and it cannot have appeared before (that would be a return after a gap). So each of the $L$ transitions spends a fresh symbol beyond the initial $d$ . This is the set-valued form of Santos' Proposition 3.10 for injective connected layer multifamilies, and the specialization of the saturated-homogeneous quadratic bound to singleton blocks. It is sharp: the sliding window $\{t,\dots,t+d-1\}$ .

Preamble

import Mathlib
import Definitions.Def_Hirsch_clf

Formal statement

namespace Hirsch

theorem clf_singleton_layers_linear
    {V : Type*} [DecidableEq V] [Fintype V] (d : ℕ) (hd : 1 ≤ d)
    (F : CLF V d) (hsingle : ∀ t, (F.layer t).card = 1) :
    F.len ≤ Fintype.card V - d := by sorry

end Hirsch

Source

F. Santos, TOP 21 (2013), arXiv:1307.5900, Section 3 Proposition 3.10; Campaign research notes (2026-09-13), Prove2Me mission 'The Polynomial Hirsch Conjecture', reports plans/clf_reduce.md, clf_construct.md, clf_polytopal.md with independent adversarial audits (plans/audit_ridge_closure.md, audit_sat_rank2.md, audit_polytopal_axioms.md), clf_reduce.md Proposition 2.1 (audited)

View graph

Connected layer families with one base per layer have length at most n−dn-dn−d

Connected layer families with one base per layer have length at most $n-d$