Prove2Me

Every connected layer family reduces to a ridge-closed one with loss factor n−d+1n-d+1

Open
Hirsch.clf_ridge_closure_reduction

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

combinatoricsconnected-layer-familieshirsch-conjecture

Retired 2026-09-13: superseded by Hirsch.clf_reduces_to_ridge_closed, which states the same reduction against the shared definition Hirsch_clf_ridge_closed instead of a private copy of the ridge-closed predicate (the private copy prevented proofs from being checked against the statement).

Preamble
import Mathlib
import Definitions.Def_Hirsch_clf
Formal statement
namespace Hirsch

/-- A layer is *ridge-closed* if it contains every `d`-set all of whose `(d-1)`-subsets lie
in some base of the layer. -/
def CLF.RidgeClosed {V : Type*} [DecidableEq V] [Fintype V] {d : ℕ} (F : CLF V d) : Prop :=
  ∀ t, ∀ B : Finset V, B.card = d →
    (∀ R ⊆ B, R.card = d - 1 → ∃ B' ∈ F.layer t, R ⊆ B') → B ∈ F.layer t

theorem clf_ridge_closure_reduction
    {V : Type} [DecidableEq V] [Fintype V] (d : ℕ) (hd : 1 ≤ d) (hdV : d ≤ Fintype.card V)
    (F : CLF V d) :
    ∃ G : CLF V d, CLF.RidgeClosed G ∧
      F.len + 1 ≤ (Fintype.card V - d + 1) * (G.len + 1) := 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_reduce.md Theorem 4.1 (audited SOUND); F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Diameter of polyhedra: limits of abstraction, Math. Oper. Res. 35 (2010); F. Santos, TOP 21 (2013), arXiv:1307.5900, Section 3

View graph