Proof of Theorem 4.2, p. 3:14 — a graph with at most N vertices has twin-width at most N

Proved

TwinWidthI.BoolWidth.twinWidth_le_of_card_le

by mikedeng1 · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

boolean-widthp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1twin-width

Let $G$ be a finite simple graph with vertex set $V$ and let $N\ge 0$ be an integer. If $G$ has at most $N$ vertices, then

\operatorname{tww}(G)\le N .

In the proof of Theorem 4.2 (with $N=2^k$ ) this disposes of graphs with at most $2^k$ vertices, so that the remaining argument may assume $|V|\ge 2^k+1$ .

Formalization Note. $\operatorname{tww}(G)\le N$ is the predicate TwinWidthLE G N of the setting (sequences of $N$ -partitions from singletons to at most one part). No lower bound on $N$ or $|V|$ is assumed; the empty graph is covered.

Preamble

import Mathlib
import Definitions.Def_TwinWidthI_BoolWidth_Setting

Formal statement

namespace TwinWidthI.BoolWidth

open Finset

theorem twinWidth_le_of_card_le {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V)
    (N : ℕ) (hcard : Fintype.card V ≤ N) : TwinWidthLE G N := by sorry

end TwinWidthI.BoolWidth

Source

Bonnet, Kim, Thomassé and Watrigant, Twin-width I: Tractable FO Model Checking, J. ACM 69(1), Article 3 (2021), p. 3:14, proof of Theorem 4.2, "otherwise the twin-width is immediately bounded by 2^k"

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph