High combinadic ranks of the $Q_{28}$ chamber certificate

Proved

Hirsch.q28_chamber_ranks_high

by jjosh · Sep 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

hirsch-conjecturepolytopesprismatoid

Let $P\subset\mathbb{R}^5$ be the polar of the Matschke--Santos--Weibel prismatoid $Q_{28}$ . In the nonnegative chamber the $\binom{14}{5}=2002$ five-row subsystems are indexed by combinadic rank.

This theorem records the high-rank half of that enumeration: every rank in $\{1100,\ldots,2001\}$ is accounted for by the stored singular, infeasible, or orbit tag.

Formalization Note The checker certOkUnrank lives in Definitions.Def_Hirsch_q28_cert.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model
import Definitions.Def_Hirsch_q28
import Definitions.Def_Hirsch_q28_cert

open scoped RealInnerProductSpace
open Hirsch

Formal statement

namespace Hirsch
theorem q28_chamber_ranks_high :
    ∀ r : ℕ, 1100 ≤ r → r < 2002 → certOkUnrank r = true := by sorry
end Hirsch

Source

B. Matschke, F. Santos, C. Weibel, The width of five-dimensional prismatoids, Proc. London Math. Soc. 110 (2015) 647-672, arXiv:1202.4701, Corollary 2.9 and the explicit

Q_{28}

vertex table.

View graph

High combinadic ranks of the Q28Q_{28}Q28​ chamber certificate

High combinadic ranks of the $Q_{28}$ chamber certificate