Lax

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax9χ-Boundedness and Neighbourhood Complexity of Bounded Merge-Width Graphs

Édouard Bonnet

created 2026-07-24·github.com/jan3er/lax-submissions@cb4d609·Lean v4.30.0 · mathlib c5ea00351c28

Abstract

This submission formalizes two results of Marthe Bonamy and Colin Geniet: every graph class of bounded merge-width is χ-bounded, and every such class has linear neighbourhood complexity, Theorems 1.2 and 1.5 of χ-Boundedness and Neighbourhood Complexity of Bounded Merge-Width Graphs (https://arxiv.org/abs/2504.08266). In particular, merge sequences, radius-rr merge-width, χ-boundedness, and neighbourhood complexity are defined in Lean.

Concepts

Dependency view
This submissionOther submission→Dependency to importer

Proofs

Derivation viewArrows follow logical support
Proven statementUnproven statementExternal node⊢ProofCycleUngrounded cycle

Proof code is not displayed; the archive records each proof's checked relationship between statements.

Cite this

@misc{Lax9,
  author = {Édouard Bonnet},
  title = {χ-Boundedness and Neighbourhood Complexity of Bounded Merge-Width Graphs},
  year = {2026},
  howpublished = {Lax Archive, Lax9},
  note = {draft},
}

References

@misc{bonamy2025chiboundedness,
  title = {χ-Boundedness and Neighbourhood Complexity of Bounded Merge-Width Graphs},
  author = {Marthe Bonamy and Colin Geniet},
  year = {2025},
  eprint = {2504.08266},
  archivePrefix = {arXiv},
  primaryClass = {math.CO},
  doi = {10.48550/arXiv.2504.08266}
}