Chamber ranks $0$ -- $1099$ of the $Q_{28}$ certificate

Proved

Hirsch.q28_chamber_ranks_0_1099

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, five-row subsystems are indexed by combinadic rank.

This theorem records that every rank in $\{0,\ldots,1099\}$ 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_0_1099 :
    ∀ r : ℕ, r < 1100 → 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.

View graph

Chamber ranks 000--109910991099 of the Q28Q_{28}Q28​ certificate

Chamber ranks $0$ -- $1099$ of the $Q_{28}$ certificate