theorem GraphColoringBound.sah_sawhney_colorings_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {d : ℕ} (hd : 0 < d) (hreg : G.IsRegularOfDegree d) (q : ℕ) : ↑(Nat.card (G.Coloring (Fin q))) ≤ ↑(Nat.card ((completeBipartiteGraph (Fin d) (Fin d)).Coloring (Fin q))) ^ (↑(Fintype.card V) / (2 * ↑d))

Theorem 10.4.15 (Sah–Sawhney–Stoner–Zhao 2020). For every $d$-regular graph $G$ on $n$ vertices and every $q \ge 1$, the number $c_q(G)$ of proper $q$-colourings satisfies $c_q(G) \le c_q(K_{d,d})^{n/(2d)}$.