Prove2Me

Common-active cards of Q28Q_{28} orbits 1010--1919 match popcount

Proved
Hirsch.q28_cardAt_eq_popcount_high

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

combinatoricspolytope-theory

The stored common-active cardinality of two Q28Q_{28} orbit labels agrees with the 2828-bit popcount of their tight-mask conjunction, for the last ten orbit indices.

Let o1,o2o_1,o_2 range over the twenty stored nonnegative orbit labels of the polar of the prismatoid Q28Q_{28}, and let ss range over the sixteen coordinatewise sign patterns. Write N(o,s)N(o,s) for the integer whose bits record the active supporting rows of the signed representative of orbit oo with signs ss, and write c(o1,o2,s)c(o_1,o_2,s) for the stored number of common active rows of the unsigned representative of o1o_1 with the ss-signed representative of o2o_2.

c(o1,o2,s)=popcount⁡28(N(o1,0)∧N(o2,s))whenever 10≤o1≤19.c(o_1,o_2,s)=\operatorname{popcount}_{28}\bigl(N(o_1,0)\land N(o_2,s)\bigr) \qquad\text{whenever }10\le o_1\le 19.

This is the high-index half of the 20×20×1620\times 20\times 16 lookup that transfers adjacency of extreme points to the stored quotient.

Formalization Note. In Lean the bound is 10 \le o1.val with o1 : Fin 20.

Preamble
import Mathlib
import Definitions.Def_Hirsch_q28_cert

open Hirsch

namespace Hirsch
Formal statement
theorem q28_cardAt_eq_popcount_high :
    ∀ (o1 o2 : Fin 20) (s : Fin 16),
      10 ≤ o1.val →
        commonActiveCard o1 o2 s =
          popcount28 (Nat.land (tightMask o1 0) (tightMask o2 s)) := by sorry
end Hirsch
Source
Santos, A counterexample to the Hirsch conjecture, arXiv:1006.2814, §2.2; Matschke--Santos--Weibel, The width of 5-dimensional prismatoids, arXiv:1202.4701, Corollary 2.9

View graph