Layer families of tight sets of a simple polytope have ridge incidence at most two

Proved

Hirsch.polytopal_clf_ridge_incidence_two

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

connected-layer-familieshirsch-conjecturepolytopes

Let $P\subseteq\mathbb R^d$ be a bounded simple H-polytope ( $d$ tight rows at every vertex) and let $F$ be any layer family whose bases are tight sets of vertices of $P$ (for instance the distance layers Hirsch.distance_layers_clf). Then every $(d-1)$ -set of rows is contained in at most two bases of the whole family.

At a simple vertex the $d$ tight normals are linearly independent, so any $d-1$ of them cut out a face of dimension one, an edge with exactly two vertices; a $(d-1)$ -set of rows tight at a vertex therefore lies in at most two tight sets. This is the polytopal incidence axiom $\rho=2$ ; with saturation it would give a linear bound (Hirsch.clf_saturated_ridge_incidence_linear_bound), but polytopal distance layers are not saturated (already the $d$ -cube fails), which locates the gap between the abstraction and the conjecture.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model
import Definitions.Def_Hirsch_walk
import Definitions.Def_Hirsch_clf

open scoped RealInnerProductSpace

Formal statement

namespace Hirsch

theorem polytopal_clf_ridge_incidence_two (d n : ℕ)
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (hbd : Bornology.IsBounded (Hpoly a b))
    (hsimple : ∀ x ∈ Set.extremePoints ℝ (Hpoly a b),
      (Finset.univ.filter (fun i : Fin n => ⟪a i, x⟫ = b i)).card = d)
    (F : CLF (Fin n) d)
    (hF : ∀ t, ∀ B ∈ F.layer t, ∃ x ∈ Set.extremePoints ℝ (Hpoly a b),
      B = Finset.univ.filter (fun i => ⟪a i, x⟫ = b i)) :
    CLF.RidgeIncidenceLE F 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_polytopal.md Theorem 2.1 (audited, audit_polytopal_axioms.md); F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Diameter of polyhedra: limits of abstraction, Math. Oper. Res. 35 (2010) (incidence axioms)

View graph