Ridge-closed connected layer families
DefinitionHirsch_clf_ridge_closedA layer of a connected layer family (definition Hirsch_clf) is ridge-closed if it contains every -set all of whose -subsets lie in some base of that layer; equivalently, the layer is determined by its ridge shadow as .
Two facts make this the natural class for the polynomial-length question of the Eisenbrand--Hähnle--Razborov--Rothvoß abstraction: every family reduces to a ridge-closed one with loss factor (Hirsch.clf_reduces_to_ridge_closed), and conversely every family is exactly the link of one symbol in a ridge-closed family of one higher rank with the same height (Hirsch.clf_cone_ridge_closed_embedding). So polynomial length for ridge-closed families is equivalent, with the same exponent, to polynomial length for all families.
Formalization Note The predicate quantifies over all layers and all -sets of the symbol type; ridges are the -subsets of the candidate base.
import Mathlib
import Definitions.Def_Hirsch_clf
/-!
# Ridge-closed connected layer families
A layer of a connected layer family is **ridge-closed** if it contains every `d`-set all of
whose `(d-1)`-subsets ("ridges") lie in some base of that layer; equivalently the layer is
determined by its ridge shadow. Every connected layer family reduces to a ridge-closed one
with polynomial loss (`Hirsch.clf_reduces_to_ridge_closed`), and conversely arbitrary
families are exactly the links of one symbol in ridge-closed families
(`Hirsch.clf_cone_ridge_closed_embedding`), so the polynomial-length question for the
Eisenbrand–Hähnle–Razborov–Rothvoß abstraction is equivalent to the same question for
ridge-closed families.
-/
namespace Hirsch
/-- Every layer of `F` contains every `d`-set all of whose `(d-1)`-subsets lie in some base
of that 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
end Hirsch