Theorem A: the bramble number bounds the gonality

This is §2 of van Dobben de Bruyn--Gijswijt (arXiv:1407.7055): for every bramble 𝔅 of a connected graph G,

order 𝔅 ≤ divisorialGonality G + 1.

Combined with Seymour--Thomas duality this gives treewidth ≤ gonality (TreewidthGonality/Gonality/TreewidthGonality.lean), but the statement here is stronger and unconditional: the bramble number of G is at least treewidth G + 1 for any graph, so this bound implies the treewidth one and holds whether or not the duality theorem has been formalized.

Conventions

Brambles live on underlyingSimpleGraph G — treewidth and brambles do not see edge multiplicities. The chip-firing side does: outdegreeSet and edgeCut count with multiplicity, which only strengthens the inequalities used here (more parallel edges make a cut more expensive, never less).

Connectivity of a vertex set is ((underlyingSimpleGraph G).induce (↑B : Set G.V)).Connected, the convention fixed in TreewidthGonality/Treewidth/TreeDecomposition.lean.

Supports and cuts

def Utilities.Gonality.divisorSupport {G : CFGraph} (D : CFDiv G) : Finset G.V

The vertices carrying at least one chip.

Equations

• Utilities.Gonality.divisorSupport D = {v : G.V | 0 < D v}

@[simp]

theorem Utilities.Gonality.mem_divisorSupport {G : CFGraph} {D : CFDiv G} {v : G.V} : v ∈ divisorSupport D ↔ 0 < D v

theorem Utilities.Gonality.card_divisorSupport_le_deg {G : CFGraph} {D : CFDiv G} (hD : effective D) : ↑(divisorSupport D).card ≤ CFDiv.degree D

An effective divisor has at least one chip on each support vertex, so the support is no bigger than the degree.

def Utilities.Gonality.edgeCut (G : CFGraph) (U : Finset G.V) : ℤ

The number of edges leaving U, counted with multiplicity.

Equations

• Utilities.Gonality.edgeCut G U = ↑(Utilities.edgesBetween G U Uᶜ)

theorem Utilities.Gonality.edgeCut_nonneg {G : CFGraph} (U : Finset G.V) : 0 ≤ edgeCut G U

theorem Utilities.Gonality.edgeCut_eq_sum_outdeg {G : CFGraph} (U : Finset G.V) : edgeCut G U = ∑ v ∈ U, outdegreeSet G U v

The cut is the total boundary of the vertices of U.

The three lemmas of §2

theorem Utilities.Gonality.support_containment {G : CFGraph} {D : CFDiv G} {U B : Finset G.V} (hD : effective D) (hBconn : (SimpleGraph.induce (↑B) (underlyingSimpleGraph G)).Connected) (hmeet : (B ∩ divisorSupport D).Nonempty) (hmiss : B ∩ divisorSupport (setFiring G D U) = ∅) : B ⊆ U

Lemma 2.2 (support containment). If firing U clears the support off a connected set B that previously met the support, then B was contained in U.

Proved (2026-08-25); the paper's argument in two steps:

1. Chips outside the fired set never decrease (le_set_firing_apply_of_not_mem), so any w ∈ B ∖ U with D w > 0 would still carry a chip after firing, contradicting hmiss. Hence B ∩ divisorSupport D ⊆ U, and by hmeet the intersection B ∩ U is nonempty.
2. If B ⊄ U, connectedness of B gives an edge of underlyingSimpleGraph G inside B with one end u ∈ U and the other end w ∈ B ∖ U (Utilities.Treewidth.exists_adj_across_of_walk). Then setFiring G D U w = D w + outdegreeSet G Uᶜ w ≥ 0 + numEdges G w u > 0, again contradicting hmiss.

Note no legality hypothesis is needed: only effectivity of D and the two set_firing_apply_* formulas.

theorem Utilities.Gonality.hitting_of_cut {G : CFGraph} (𝔅 : Treewidth.Bramble (underlyingSimpleGraph G)) {U B B' : Finset G.V} (hB : B ∈ 𝔅.members) (hB' : B' ∈ 𝔅.members) (hBU : B ⊆ U) (hB'U : B' ⊆ Uᶜ) : ↑𝔅.order ≤ edgeCut G U + 1

Lemma 2.3 (a cut separating two members bounds the order). If a bramble has a member inside U and a member inside the complement of U, then its order is at most one more than the number of edges crossing the cut.

Proved (2026-08-25) following the paper's §2 verbatim (Lemma 2.3 there, where the containments are named the other way round: their B' is our B).

The naive hitting set "all endpoints of cut edges" has size edgeCut + (components of the cut graph), so it overshoots. The paper's construction, reproduced here, is one endpoint per cut edge plus one extra vertex, and the choice that makes the case analysis close is:

• let X, Y be the two shores of the cut and, among all members contained in U, let B₀ be one whose trace B₀ ∩ X is inclusionwise minimal (realized here by minimizing (B₀ ∩ X).card) — this is the step that is easy to miss and without which the lemma's case 1 is false;
• let s be any vertex of B₀ ∩ X (nonempty because B₀ touches B');
• for each cut edge xy with x ∈ X, y ∈ Y, select x if x ∉ B₀ and y otherwise; S is the selection together with s, so |S| ≤ edgeCut + 1.

S hits every member A:

• A ∩ Y = ∅: then A ⊆ U, so A is a competitor for the minimality of B₀ ∩ X. Either some x ∈ (A ∩ X) ∖ B₀, and then x was selected for its own cut edge, or A ∩ X ⊆ B₀ ∩ X, whence A ∩ X = B₀ ∩ X by minimality and s ∈ A.
• A ∩ X = ∅: then A ⊆ Uᶜ, and the cut edge joining A to B₀ has its U-end in B₀, so its Uᶜ-end — a vertex of A — was selected.
• both nonempty: connectedness puts a whole cut edge inside A, and one of its ends was selected.

The multiplicity convention only helps: the cut is modelled by the finite set of ordered pairs (x, y) ∈ U × Uᶜ with numEdges > 0, whose cardinality is at most edgeCut.

theorem Utilities.Gonality.charge_of_legal {G : CFGraph} {D : CFDiv G} {U : Finset G.V} (hU : legalSet G D U) : edgeCut G U ≤ ∑ v ∈ U, D v

The charge of a legal set. A legally fired set pays one chip per edge leaving it, so it must have been carrying at least edgeCut G U chips.

theorem Utilities.Gonality.edgeCut_le_deg_of_legal {G : CFGraph} {D : CFDiv G} {U : Finset G.V} (hD : effective D) (hU : legalSet G D U) : edgeCut G U ≤ CFDiv.degree D

The degree of an effective divisor bounds any cut it can legally fire.

Theorem A

theorem Utilities.Gonality.bramble_order_le_gonality_succ {G : CFGraph} (h_conn : graphConnected G) (𝔅 : Treewidth.Bramble (underlyingSimpleGraph G)) : 𝔅.order ≤ divisorialGonality G + 1

Theorem A (van Dobben de Bruyn--Gijswijt §2). Every bramble of a connected graph has order at most divisorialGonality G + 1.

Proved (2026-08-25); this is the main theorem of §2 of the paper. The proof narrative, matching the code line for line:

Let d = divisorialGonality G. Among all effective divisors D of degree d with rank G D ≥ 1 (a nonempty finite-to-choose-from family: nonempty by exists_divisor_of_divisorialGonality), choose one maximizing the number of members of 𝔅 that divisorSupport D hits. This is a finite extremal choice: the quantity being maximized is (𝔅.members.filter fun B => (B ∩ divisorSupport D).Nonempty).card, bounded by 𝔅.members.card.

Case 1: divisorSupport D hits every member. Then divisorSupport D is a hitting set, so 𝔅.order ≤ (divisorSupport D).card ≤ deg D = d by Bramble.order_le_card_of_isHittingSet and card_divisorSupport_le_deg — even better than claimed.

Case 2: some member B₀ is unhit. Pick v ∈ B₀ (members are nonempty, Bramble.nonempty_of_mem). Run the nested legal chain of exists_nested_legal_chain at q = v: sets U 0 ⊆ U 1 ⊆ … ⊆ U (k-1) ⊆ univ.erase v with divisors Dᵢ = fireChain G D U i, every Dᵢ effective (fireChain_effective), every Dᵢ linearly equivalent to D (fireChain_linear_equiv, so deg Dᵢ = d and rank G Dᵢ ≥ 1), and D_k v-reduced. By one_le_apply_of_q_reduced_of_rank_geq_one, D_k v ≥ 1, so D_k does hit B₀.

Let i be the first index at which the family of members hit by D fails to be contained in the family hit by D_i. Such an i exists: otherwise the hit family only grows along the chain, while B₀ is newly hit at the end, so D_k would hit strictly more members than D, contradicting the extremal choice of D (D_k is a competitor: effective, degree d, rank ≥ 1). Note i ≥ 1 because D_0 = D.

Write U = U (i-1), B' for the member hit by D (hence, by minimality of i, also by D_{i-1}) and unhit by D_i. Then:

• support_containment applied to D_{i-1}, U, B' gives B' ⊆ U;
• B₀ ⊆ Uᶜ, by the paper's second index: maximality of D also forces B₀ ∩ supp D_{i-1} = ∅ (otherwise D_{i-1} hits strictly more members than D), and B₀ is hit by D_k, so there is a first j ≥ i-1 with B₀ ∩ supp D_j = ∅ and B₀ ∩ supp D_{j+1} ≠ ∅. Since firing (U j)ᶜ undoes firing U j (set_firing_compl_set_firing), support_containment applied to D_{j+1} and the fired set (U j)ᶜ gives B₀ ⊆ (U j)ᶜ ⊆ (U (i-1))ᶜ by nestedness.
• hitting_of_cut for the pair (B', B₀) gives 𝔅.order ≤ edgeCut G U + 1;
• charge_of_legal/edgeCut_le_deg_of_legal for the legal set U at D_{i-1} gives edgeCut G U ≤ deg D_{i-1} = d.

Hence 𝔅.order ≤ d + 1 in both cases.

The extremal choice is realized as Nat.sSup of the (nonempty, bounded by 𝔅.members.card) set of achievable hit counts, which avoids having to know that the family of competitors is finite.