The burned set, without Dhar's algorithm

Dhar's burning algorithm takes (G, D, q) and returns the maximal valid set A ⊆ V(G) \ {q}; the burned vertices are the complement of A. Every use of the algorithm in the divisorial-gonality literature is a use of exactly two of its properties — maximality of A, and the rule "a vertex with fewer chips than burned incident edges burns" — and both are available without running anything.

The dependency's legal_set_union says legal sets are closed under union, so the maximal legal subset of V \ {q} is a Finset.sup over a powerset:

• maximalLegal G D q — the join of every legal U ⊆ univ.erase q;
• burned G D q := (maximalLegal G D q)ᶜ — the burned set.

The API below is the whole of Dhar that the tricycle campaign (the accompanying analysis §4.1) ever uses:

• legalSet_maximalLegal, subset_maximalLegal_of_legal — maximality;
• mem_burned_self, mem_burned_of_lt, mem_burned_of_subset_lt, mem_burned_of_mem_burned_adj — the burning rule;
• sum_burned_le_of_not_mem_burned — the converse rule, which is what turns "v is unburned" into a chip count;
• qReduced_iff_maximalLegal_eq_empty — the fire consumes everything exactly when D is q-reduced;
• mem_maximalLegal_of_qReduced — Lemma 3.5(a) of van Dobben de Bruyn–Smit–van der Wegen, in full generality: a q-reduced divisor's own q is never burned by a fire started anywhere else.

No algorithm, no termination proof, no fuel. maximalLegal is noncomputable and is only ever used propositionally; never decide it (blueprint risk R2).

The maximal legal set

@[irreducible]

noncomputable def Utilities.Gonality.maximalLegal (G : CFGraph) (D : CFDiv G) (q : G.V) : Finset G.V

The maximal legal subset of V \ {q}: the join of all of them. It is legal because legal sets are closed under union (legal_set_union).

Equations

• Utilities.Gonality.maximalLegal G D q = {U ∈ (Finset.univ.erase q).powerset | legalSet G D U}.sup id

@[irreducible]

noncomputable def Utilities.Gonality.burned (G : CFGraph) (D : CFDiv G) (q : G.V) : Finset G.V

The burned set of (G, D, q): the complement of the maximal legal set. This is what Dhar's burning algorithm computes.

Equations

• Utilities.Gonality.burned G D q = (Utilities.Gonality.maximalLegal G D q)ᶜ

theorem Utilities.Gonality.maximalLegal_subset {G : CFGraph} {D : CFDiv G} {q : G.V} : maximalLegal G D q ⊆ Finset.univ.erase q

theorem Utilities.Gonality.legalSet_maximalLegal {G : CFGraph} {D : CFDiv G} {q : G.V} : legalSet G D (maximalLegal G D q)

The join of legal sets is legal.

theorem Utilities.Gonality.subset_maximalLegal_of_legal {G : CFGraph} {D : CFDiv G} {q : G.V} {U : Finset G.V} (hU : legalSet G D U) (hq : U ⊆ Finset.univ.erase q) : U ⊆ maximalLegal G D q

Maximality: every legal set avoiding q is contained in maximalLegal.

theorem Utilities.Gonality.not_mem_maximalLegal_self {G : CFGraph} {D : CFDiv G} {q : G.V} : q ∉ maximalLegal G D q

The burned set

@[simp]

theorem Utilities.Gonality.mem_burned_iff {G : CFGraph} {D : CFDiv G} {q : G.V} (v : G.V) : v ∈ burned G D q ↔ v ∉ maximalLegal G D q

theorem Utilities.Gonality.mem_burned_self {G : CFGraph} {D : CFDiv G} {q : G.V} : q ∈ burned G D q

The source of the fire is burned.

theorem Utilities.Gonality.outdeg_maximalLegal {G : CFGraph} {D : CFDiv G} {q : G.V} (v : G.V) : outdegreeSet G (maximalLegal G D q) v = ∑ w ∈ burned G D q, ↑(numEdges G v w)

The edges from v into the burned set, as an integer.

theorem Utilities.Gonality.sum_burned_le_of_not_mem_burned {G : CFGraph} {D : CFDiv G} {q v : G.V} (hv : v ∉ burned G D q) : ∑ w ∈ burned G D q, ↑(numEdges G v w) ≤ D v

The converse burning rule. An unburned vertex can afford every one of its edges into the fire.

theorem Utilities.Gonality.mem_burned_of_lt {G : CFGraph} {D : CFDiv G} {q v : G.V} (h : D v < ∑ w ∈ burned G D q, ↑(numEdges G v w)) : v ∈ burned G D q

The burning rule. A vertex with fewer chips than burned incident edges burns. This is all of Dhar's algorithm that any proof here needs.

theorem Utilities.Gonality.mem_burned_of_subset_lt {G : CFGraph} {D : CFDiv G} {q v : G.V} {S : Finset G.V} (hS : S ⊆ burned G D q) (h : D v < ∑ w ∈ S, ↑(numEdges G v w)) : v ∈ burned G D q

The burning rule against any subset of the fire.

theorem Utilities.Gonality.mem_burned_of_mem_burned_adj {G : CFGraph} {D : CFDiv G} {q u v : G.V} (hu : u ∈ burned G D q) (h : D v < ↑(numEdges G v u)) : v ∈ burned G D q

The burning rule against one burned neighbour.

theorem Utilities.Gonality.mem_burned_of_two_adj {G : CFGraph} {D : CFDiv G} {q u u' v : G.V} (hu : u ∈ burned G D q) (hu' : u' ∈ burned G D q) (hne : u ≠ u') (h : D v < ↑(numEdges G v u) + ↑(numEdges G v u')) : v ∈ burned G D q

The burning rule against two distinct burned neighbours.

The fire consumes everything exactly on q-reduced divisors

theorem Utilities.Gonality.maximalLegal_eq_empty_iff {G : CFGraph} {D : CFDiv G} {q : G.V} : maximalLegal G D q = ∅ ↔ ∀ S ⊆ Finset.univ.erase q, S.Nonempty → ¬legalSet G D S

theorem Utilities.Gonality.qReduced_iff_maximalLegal_eq_empty {G : CFGraph} {D : CFDiv G} {q : G.V} (hEff : qEffective q D) : qReduced G q D ↔ maximalLegal G D q = ∅

The q-reduced predicate of the chip-firing dependency says, verbatim, that no nonempty subset of V \ {q} is legal. Hence: the fire started at q consumes the whole graph exactly when D is q-reduced.

theorem Utilities.Gonality.burned_eq_univ_iff {G : CFGraph} {D : CFDiv G} {q : G.V} (hEff : qEffective q D) : burned G D q = Finset.univ ↔ qReduced G q D

Lemma 3.5(a) of van Dobben de Bruyn–Smit–van der Wegen

theorem Utilities.Gonality.mem_maximalLegal_of_qReduced {G : CFGraph} {D : CFDiv G} {q : G.V} (hred : qReduced G q D) {w : G.V} (hne : (maximalLegal G D w).Nonempty) : q ∈ maximalLegal G D w

If the fire started at w leaves anything unburned, then a q-reduced divisor's own base point q is among the survivors.

This is Lemma 3.5(a) of van Dobben de Bruyn–Smit–van der Wegen, in the generality in which it is true: the maximal legal set is legal and nonempty, and a q-reduced divisor admits no nonempty legal set avoiding q.

theorem Utilities.Gonality.maximalLegal_nonempty_of_rank_ge_one {G : CFGraph} {D : CFDiv G} (hEff : effective D) (hrank : rank G D ≥ 1) {w : G.V} (hw : D w = 0) : (maximalLegal G D w).Nonempty

The fire started at a chip-free vertex of a positive-rank divisor never consumes the whole graph.

theorem Utilities.Gonality.not_mem_burned_of_qReduced {G : CFGraph} {D : CFDiv G} {q : G.V} (hEff : effective D) (hred : qReduced G q D) (hrank : rank G D ≥ 1) {w : G.V} (hw : D w = 0) : q ∉ burned G D w

Lemma 3.5(a), assembled: for a positive-rank q-reduced divisor and a chip-free vertex w, the vertex q is not burned by the fire started at w.

Opacity

maximalLegal is a Finset.sup over the powerset of univ.erase q. Left reducible, any isDefEq check between two x ∈ burned G D q types whose vertices are closed terms (a Fin numeral, a Sum.inl, a Fin.mk) falls through congruence and starts evaluating Finset.univ, List.erase and instDecidableEqSum.decEq on the subdivision vertex type. Since the whole point of the design is that maximalLegal is used propositionally only sealing both definitions costs nothing and makes every such comparison structural. Everything above this line is stated and proved before the seal; nothing below may unfold either definition.