Rank-two connected layer families of height $2n-\log_2 n-2$ on $n=2^k$ symbols

Proved

Hirsch.clf_rank_two_doubling_family

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

combinatoricsconnected-layer-familieshirsch-conjecture

For every $k\ge1$ there is a connected layer family of rank $2$ on $2^k$ symbols with height $L+1=2\cdot2^k-k-2$ (each layer a matching, every edge of $K_{2^k}$ used once, every vertex active on an interval of layers).

The construction doubles a proper interval edge-colouring of $K_m$ to one of $K_{2m}$ with $2m-1$ more colours (Khachatrian--Petrosyan), which is exactly the rank-two connected layer axiom. For $n\ge8$ these families exceed the exact maximum $2n-\lceil2\sqrt n\rceil$ of the saturated homogeneous class, so no fixed partition makes them saturated: non-saturation genuinely lengthens layer families, by $\Theta(\sqrt n)$ at rank two, while remaining linear.

Preamble

import Mathlib
import Definitions.Def_Hirsch_clf

Formal statement

namespace Hirsch

theorem clf_rank_two_doubling_family (k : ℕ) (hk : 1 ≤ k) :
    ∃ F : CLF (Fin (2 ^ k)) 2, F.len + 1 = 2 * 2 ^ k - k - 2 := by sorry

end Hirsch

Source

H. H. Khachatrian, P. A. Petrosyan, Interval edge-colorings of complete graphs, Discrete Math. 339 (2016); 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_construct.md Section 5.2 (audited)

View graph

Rank-two connected layer families of height 2n−log⁡2n−22n-\log_2 n-22n−log2​n−2 on n=2kn=2^kn=2k symbols

Rank-two connected layer families of height $2n-\log_2 n-2$ on $n=2^k$ symbols