Exact maximum lengths of rank-two connected layer families on 5, 6 and 8 symbols

Proved

Hirsch.clf_rank_two_small_optima

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

combinatoricsconnected-layer-familieshirsch-conjecture

The maximum length of a connected layer family of rank $2$ is exactly $4$ on $5$ symbols, $6$ on $6$ symbols and $10$ on $8$ symbols. Rank-two families are edge-labelled simple graphs in which every vertex's labels form an interval (improper interval edge-colourings, edges sharing a vertex may share a label), and these optima were found by exact SAT search with DRAT-verified unsatisfiability certificates for one more layer; the witnesses are explicit matchings (for $n=8$ : eleven layers using all $28$ edges of $K_8$ ). On $8$ symbols the optimum exceeds the saturated homogeneous maximum $10$ layers by one, the smallest separation between the two classes.

Formalization Note Both existence (explicit finite family, checkable by decide) and the upper bound (a finite search over all families, which the kernel must carry out or which must be replaced by a counting argument) are asserted; the upper bounds are the substantial part.

Preamble

import Mathlib
import Definitions.Def_Hirsch_clf

Formal statement

namespace Hirsch

theorem clf_rank_two_small_optima :
    (∃ F : CLF (Fin 8) 2, F.len = 10) ∧ (∀ F : CLF (Fin 8) 2, F.len ≤ 10) ∧
    (∃ F : CLF (Fin 6) 2, F.len = 6) ∧ (∀ F : CLF (Fin 6) 2, F.len ≤ 6) ∧
    (∃ F : CLF (Fin 5) 2, F.len = 4) ∧ (∀ F : CLF (Fin 5) 2, F.len ≤ 4) := by sorry

end Hirsch

Source

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 3 (SAT certificates in plans/clf_search/certificates, audited)

View graph