treewidth ≤ gonality

The theorem of van Dobben de Bruyn--Gijswijt (arXiv:1407.7055): the treewidth of a connected graph is at most its divisorial gonality.

The proof is the two-line composition of the repository's two halves:

• Utilities.Gonality.bramble_order_le_gonality_succ — Theorem A, the divisor-theoretic heart (#print axioms reports exactly [propext, Classical.choice, Quot.sound]);
• Utilities.Treewidth.exists_bramble_of_treewidth — Seymour--Thomas duality, following Bellenbaum--Diestel's short proof; see TreewidthGonality/Treewidth/SeymourThomas.lean.

Both halves are unconditional, so #print axioms on the theorems below reports exactly [propext, Classical.choice, Quot.sound].

theorem Utilities.Gonality.treewidth_le_gonality {G : CFGraph} (h_conn : graphConnected G) : Treewidth.treewidth (underlyingSimpleGraph G) ≤ divisorialGonality G

treewidth ≤ gonality (van Dobben de Bruyn--Gijswijt). Treewidth is taken on underlyingSimpleGraph G, which is what "the treewidth of a multigraph" means: parallel edges and loops do not change it.

theorem Utilities.Gonality.treewidth_le_gonality_int {G : CFGraph} (h_conn : graphConnected G) : ↑(Treewidth.treewidth (underlyingSimpleGraph G)) ≤ gonality h_conn

The same bound against the dependency's ℤ-valued gonality.