Exact maximum length of saturated homogeneous connected layer families of rank two

Disproved

Hirsch.clf_saturated_rank_two_exact

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

combinatoricsconnected-layer-familieshirsch-conjecture

For rank $d=2$ and $n\ge2$ symbols, the maximum height $L+1$ over all block partitions and all saturated homogeneous connected layer families (the class of the quadratic bound Hirsch.clf_saturated_quadratic_bound) is exactly

h_{\mathrm{sat}}(n,2)=2n-\varepsilon-\bigl\lceil 2\sqrt{n-\varepsilon}\,\bigr\rceil,\qquad \varepsilon=n\bmod 2 .

The upper bound counts pure layers of a block (edge covers of $K_m$ by disjoint edge sets, at most $m-1$ or $m-2$ ) and mixed layers between two blocks (at most $\min(a,b)$ ), shows the block-interval intersection graph is a forest, and optimizes $q+M$ over partitions, which yields the $\lceil2\sqrt n\rceil$ term. The bound is attained by one-factorizations of even blocks joined by the colour classes $i+j \bmod a$ of complete bipartite graphs between consecutive blocks.

Since unrestricted rank-two families reach height $11$ on $8$ symbols against $10$ for the saturated class, this is the first exact separation between the saturated class and general connected layer families; the gap grows like $\sqrt n$ (Hirsch.clf_rank_two_doubling_family).

Formalization Note Both directions are stated: the bound for every finite block type and partition, and an attaining family for some block type.

Preamble

import Mathlib
import Definitions.Def_Hirsch_clf

Formal statement

namespace Hirsch

theorem clf_saturated_rank_two_exact (n : ℕ) (hn : 2 ≤ n) :
    (∀ (G : Type) [DecidableEq G] [Fintype G] (blk : Fin n → G) (F : CLF (Fin n) 2),
      CLF.IsSaturatedHomogeneous blk F →
      F.len + 1 ≤ 2 * n - n % 2 - Nat.ceil (2 * Real.sqrt (n - n % 2 : ℝ))) ∧
    ∃ (G : Type) (_ : DecidableEq G) (_ : Fintype G) (blk : Fin n → G) (F : CLF (Fin n) 2),
      CLF.IsSaturatedHomogeneous blk F ∧
      F.len + 1 = 2 * n - n % 2 - Nat.ceil (2 * Real.sqrt (n - n % 2 : ℝ)) := 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 Theorem 4.1 (audited SOUND, audit_sat_rank2.md)

View graph