Ridge-closed connected layer families of rank two have length exactly at most
ProvedHirsch.clf_rank_two_ridge_closed_exactcombinatoricsconnected-layer-familieshirsch-conjecture
For rank on symbols, a ridge-closed layer is a clique on its active symbols (a pair whose two singletons are active must be present). The maximum length of a ridge-closed connected layer family of rank two is exactly : the bound because consecutive cliques must be edge-disjoint and each symbol's activity is an interval, so each transition retires or introduces a symbol; attained by the sliding pairs . This is far below the unrestricted rank-two optima (which reach , Hirsch.clf_rank_two_doubling_family), showing that ridge-closure genuinely shortens families at fixed rank even though it is exponent-preserving across ranks.
Preamble
import Mathlib import Definitions.Def_Hirsch_clf import Definitions.Def_Hirsch_clf_ridge_closed
Formal statement
namespace Hirsch
theorem clf_rank_two_ridge_closed_exact
{V : Type*} [DecidableEq V] [Fintype V] (hV : 2 ≤ Fintype.card V) :
(∀ F : CLF V 2, CLF.RidgeClosed F → F.len + 2 ≤ Fintype.card V) ∧
∃ F : CLF V 2, CLF.RidgeClosed F ∧ F.len + 2 = Fintype.card V := by sorry
end HirschSource
Campaign research notes (2026-09-13), plans/rc_charge.md, rc_search.md, rc_lowerbound.md with adversarial audits (plans/audit_rc_*.md); F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Math. Oper. Res. 35 (2010); F. Santos, TOP 21 (2013) Section 3