Legal set firings and the nested reduction chain

This module supplies the divisor-theoretic input of the van Dobben de Bruyn--Gijswijt proof that treewidth ≤ gonality: their Lemma 1.3, which says that an effective divisor can be driven to its q-reduced form through a nested chain of legal set firings, every intermediate divisor effective.

The dependency (chip-firing-with-lean) supplies the legal-set vocabulary, set-firing formulas, script primitives, and reduced-divisor chip test. What it does not yet supply is the truncation lemma or nestedness of the firing sets, which is what the extremal argument in TreewidthGonality/Gonality/BrambleGonality.lean needs.

Conventions (multiplicity!)

outdegreeSet G U v = ∑_{u ∉ U} numEdges G v u counts with edge multiplicity, matching both setFiring and the dependency's qReduced. Firing every vertex of U exactly once satisfies

• setFiring G D U v = D v - outdegreeSet G U v for v ∈ U;
• setFiring G D U v = D v + outdegreeSet G Uᶜ v for v ∉ U

— chips only ever leave the fired set and only ever arrive outside it.

A set U is legal for D when firing it keeps D effective, i.e. D u ≥ outdegreeSet G U u for all u ∈ U.

Firing scripts and truncation

The nested chain below is obtained as the level-set decomposition of the firing script that carries D to its q-reduced representative, so this section records the one remaining piece of script calculus it needs.

theorem Utilities.Gonality.set_firing_compl_set_firing {G : CFGraph} (D : CFDiv G) (U : Finset G.V) : setFiring G (setFiring G D U) Uᶜ = D

Firing everything once changes nothing, so firing Uᶜ undoes firing U. This is what turns the step Dⱼ₋₁ → Dⱼ around in the main theorem: Dⱼ₋₁ is obtained from Dⱼ by firing the complement of U j.

theorem Utilities.Gonality.effective_add_prin_truncate {G : CFGraph} {D : CFDiv G} {x : firingScript G} (hD : effective D) (hDx : effective (D + (prin G) x)) (c : ℤ) : effective (D + (prin G) fun (v : G.V) => max (x v - c) 0)

The truncation lemma. If D and D + prin G x are both effective then so is every intermediate divisor obtained by truncating the script from below: D + prin G (x - c)⁺ is effective for every c.

This is the whole content of the nested chain: the level sets of x fire in increasing order and every partial sum is such a truncation.

Iterated firing

def Utilities.Gonality.fireChain (G : CFGraph) (D : CFDiv G) (U : ℕ → Finset G.V) : ℕ → CFDiv G

fireChain G D U i is the result of firing U 0, U 1, …, U (i-1) in turn.

Equations

• Utilities.Gonality.fireChain G D U 0 = D
• Utilities.Gonality.fireChain G D U i.succ = setFiring G (Utilities.Gonality.fireChain G D U i) (U i)

@[simp]

theorem Utilities.Gonality.fireChain_zero {G : CFGraph} (D : CFDiv G) (U : ℕ → Finset G.V) : fireChain G D U 0 = D

@[simp]

theorem Utilities.Gonality.fireChain_succ {G : CFGraph} (D : CFDiv G) (U : ℕ → Finset G.V) (i : ℕ) : fireChain G D U (i + 1) = setFiring G (fireChain G D U i) (U i)

theorem Utilities.Gonality.fireChain_linear_equiv {G : CFGraph} (D : CFDiv G) (U : ℕ → Finset G.V) (i : ℕ) : linearEquiv G D (fireChain G D U i)

Every divisor in a firing chain is linearly equivalent to the initial one.

theorem Utilities.Gonality.fireChain_effective {G : CFGraph} {D : CFDiv G} (hD : effective D) {U : ℕ → Finset G.V} {k : ℕ} (hlegal : ∀ i < k, legalSet G (fireChain G D U i) (U i)) (i : ℕ) : i ≤ k → effective (fireChain G D U i)

Every divisor in a chain of legal firings is effective.

The nested chain (van Dobben de Bruyn--Gijswijt, Lemma 1.3)

theorem Utilities.Gonality.exists_nested_legal_chain {G : CFGraph} (h_conn : graphConnected G) (q : G.V) {D : CFDiv G} (hD : effective D) : ∃ (k : ℕ) (U : ℕ → Finset G.V), (∀ i < k, U i ⊆ Finset.univ.erase q) ∧ (∀ i < k, (U i).Nonempty) ∧ (∀ (i j : ℕ), i ≤ j → j < k → U i ⊆ U j) ∧ (∀ i < k, legalSet G (fireChain G D U i) (U i)) ∧ qReduced G q (fireChain G D U k)

The nested legal chain. From an effective divisor D and a vertex q there is a finite chain of legal firings, with the fired sets nested and avoiding q, whose end result is q-reduced.

Proved (2026-08-25); this is Lemma 1.3 of van Dobben de Bruyn--Gijswijt (arXiv:1407.7055), and only existence is claimed — the paper never uses uniqueness of the chain.

The route actually taken is the paper's level-set decomposition, not the "maximal legal set" route this docstring used to recommend. That route is a dead end: a set U legal for D is not in general legal for setFiring G D U (that would need D u ≥ 2 · outdegreeSet G U u), so maximality at consecutive steps does not force nestedness. What works instead:

• take D', the q-reduced representative of D (exists_q_reduced_representative), effective because D is (effective_of_winnable_and_q_reduced);
• write D' = D + prin G x and normalize the script by x q = 0 (prin_sub_const);
• x ≥ 0: the bottom level set W = {v | x v = min x} is legal for D' — it is the first firing of the reverse chain, so effective_add_prin_truncate applies — and a q-reduced divisor admits no nonempty legal subset of univ.erase q, forcing q ∈ W, i.e. min x = x q = 0;
• the chain is the level-set family U i = {v | K - i ≤ x v} with K = max x, fired in increasing order i = 0, …, K-1. Its partial sums are exactly the truncations (x - (K - t))⁺, so effective_add_prin_truncate makes every intermediate divisor effective, which is the same thing as legality of each step; and the last truncation is x itself, so the chain ends at D'.

The only real content is effective_add_prin_truncate, four lines of case analysis on x v ≤ c.