Configurations and superstable configurations

Fix a vertex $q \in G.V$. A configuration (Config G q) is a nonnegative integer assignment to the vertices G.V \ {q}, extended by zero at $q$. This corresponds to what [Corry-Perkinson] calls a nonnegative configuration (Definition 2.9); we use "configuration" to mean "nonnegative configuration" throughout this library.

A configuration $c$ is superstable if for every nonempty $S \subseteq G.V \setminus \{q\}$, some vertex in $S$ has fewer chips than its out-degree into G.V \ S ([Corry-Perkinson], Definition 3.12). By superstable_iff_q_reduced, this is equivalent to the associated divisor being $q$-reduced. A maximal superstable configuration is one that is not dominated by any other superstable configuration.

The set outdeg_S G q S v counts edges from v to vertices outside S, and is the relevant threshold for the superstability condition.

@[reducible, inline]

abbrev Vtilde {G : CFGraph} (q : G.V) : Finset G.V

The set of vertices other than q: $\tilde{V} = G.V \setminus \{q\}$.

Equations

• Vtilde q = {v : G.V | v ≠ q}

structure Config (G : CFGraph) (q : G.V) : Type u_1

A configuration on G with respect to distinguished vertex q is a nonnegative integer assignment to all vertices, with the convention that q holds zero chips. This is what [Corry-Perkinson] calls a nonnegative configuration (Definition 2.9).

• vertex_degree : CFDiv G

  Assignment of integers to vertices representing the number of chips at each vertex

• q_zero : self.vertex_degree q = 0

  Fix vertex_degree q = 0 for convenience

• non_negative (v : G.V) : self.vertex_degree v ≥ 0

  Proof that all vertices except q have non-negative values

def config_degree {G : CFGraph} {q : G.V} (c : Config G q) : ℤ

The degree of a configuration is the sum of all values except at q. deg(c) = ∑_{v ∈ G.V{q}} c(v)

Equations

• config_degree c = deg c.vertex_degree

def toDiv {G : CFGraph} {q : G.V} (d : ℤ) (c : Config G q) : CFDiv G

Convert a configuration c to a divisor of prescribed degree d by placing d - config_degree c chips at q.

Equations

• toDiv d c = c.vertex_degree + (d - config_degree c) • one_chip q

theorem eq_config_iff_eq_vertex_degree {G : CFGraph} {q : G.V} (c₁ c₂ : Config G q) : c₁ = c₂ ↔ c₁.vertex_degree = c₂.vertex_degree

Two configurations are equal iff their vertex_degree functions agree.

theorem eq_config_iff_eq_div {G : CFGraph} {q : G.V} (d : ℤ) (c₁ c₂ : Config G q) : c₁ = c₂ ↔ toDiv d c₁ = toDiv d c₂

Two configurations are equal iff their images under toDiv d agree.

def to_qed {G : CFGraph} {q : G.V} (d : ℤ) (c : Config G q) : q_eff_div G q

Convert a configuration c to the $q$-effective divisor toDiv d c, bundled with its proof of $q$-effectivity.

Equations

• to_qed d c = { D := toDiv d c, h_eff := ⋯ }

def toConfig {G : CFGraph} {q : G.V} (D : q_eff_div G q) : Config G q

Convert a $q$-effective divisor to a configuration by zeroing out the chip count at q.

Equations

• toConfig D = { vertex_degree := D.D - D.D q • one_chip q, q_zero := ⋯, non_negative := ⋯ }

def config_degree_div_degree {G : CFGraph} {q : G.V} (D : q_eff_div G q) : deg D.D = D.D q + config_degree (toConfig D)

The degree of a $q$-effective divisor equals its value at q plus the configuration degree.

Equations

• ⋯ = ⋯

@[simp]

theorem toDiv_config_degree_add {G : CFGraph} {q : G.V} (c : Config G q) (k : ℤ) : toDiv (config_degree c + k) c = c.vertex_degree + k • one_chip q

Shifting the prescribed degree by k adds k chips at q.

@[simp]

theorem deg_vertex_degree_sub_one_chip {G : CFGraph} {q : G.V} (c : Config G q) : deg (c.vertex_degree - one_chip q) = config_degree c - 1

The divisor c - q has degree config_degree c - 1.

theorem div_of_config_of_div {G : CFGraph} {q : G.V} (D : q_eff_div G q) : toDiv (deg D.D) (toConfig D) = D.D

to_qed is a left inverse of toConfig at the correct degree: converting a $q$-effective divisor to a configuration and back via toDiv (deg D.D) recovers the original divisor.

@[simp]

theorem q_reduced_toDiv_toConfig (G : CFGraph) (q : G.V) (D : CFDiv G) (h_qred : q_reduced G q D) : toDiv (deg D) (toConfig { D := D, h_eff := ⋯ }) = D

A q-reduced divisor is recovered by converting to its canonical configuration and back.

theorem q_reduced_eq_vertex_degree_add_q (G : CFGraph) (q : G.V) (D : CFDiv G) (h_qred : q_reduced G q D) : D = (toConfig { D := D, h_eff := ⋯ }).vertex_degree + D q • one_chip q

A q-reduced divisor is its canonical configuration plus its chips at q.

theorem q_reduced_eq_vertex_degree_sub_one_chip (G : CFGraph) (q : G.V) (D : CFDiv G) (h_qred : q_reduced G q D) (h_q : D q = -1) : D = (toConfig { D := D, h_eff := ⋯ }).vertex_degree - one_chip q

If a q-reduced divisor has value -1 at q, it is exactly c - q for its canonical configuration c.

theorem config_eff {G : CFGraph} {q : G.V} (d : ℤ) (c : Config G q) : effective (toDiv d c) ↔ d ≥ config_degree c

The divisor toDiv d c is effective iff d ≥ config_degree c, i.e. there are enough chips at q to cover any debt.

@[implicit_reducible]

instance instPartialOrderConfig {G : CFGraph} {q : G.V} : PartialOrder (Config G q)

Equations

• instPartialOrderConfig = { le := fun (c₁ c₂ : Config G q) => c₁.vertex_degree ≤ c₂.vertex_degree, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

theorem config_eq_of_le_and_degree {G : CFGraph} {q : G.V} {c1 c2 : Config G q} (h_le : c2 ≤ c1) (h_deg : config_degree c1 = config_degree c2) : c1 = c2

Two configurations are equal if one is pointwise bounded above by the other and they have the same degree.

def outdeg_S (G : CFGraph) (q : G.V) (S : Finset G.V) (v : G.V) : ℤ

The out-degree of vertex v with respect to set S: the number of edges from v to vertices outside S. Used to define the superstability condition.

Equations

• outdeg_S G q S v = ∑ w ∈ Finset.univ \ S, ↑(num_edges G v w)

def superstable (G : CFGraph) (q : G.V) (c : Config G q) : Prop

A configuration c is superstable if for every nonempty $S \subseteq G.V \setminus \{q\}$, some vertex in $S$ has fewer chips than its out-degree into G.V \ S. [Corry-Perkinson], Definition 3.12

Equations

• superstable G q c = ∀ S ⊆ Vtilde q, S.Nonempty → ∃ v ∈ S, c.vertex_degree v < outdeg_S G q S v

theorem superstable_iff_q_reduced (G : CFGraph) (q : G.V) (d : ℤ) (c : Config G q) : superstable G q c ↔ q_reduced G q (toDiv d c)

A configuration c is superstable iff toDiv d c is $q$-reduced (for any d). [Corry-Perkinson], Remark 3.14

theorem q_reduced_toConfig_superstable (G : CFGraph) (q : G.V) (D : CFDiv G) (h_qred : q_reduced G q D) : superstable G q (toConfig { D := D, h_eff := ⋯ })

The canonical configuration of a q-reduced divisor is superstable.

theorem q_reduced_superstable_correspondence (G : CFGraph) (q : G.V) (D : CFDiv G) : q_reduced G q D ↔ ∃ (c : Config G q), superstable G q c ∧ D = toDiv (deg D) c

Helper Lemma: Equivalence between q-reduced divisors and superstable configurations. A divisor D is q-reduced iff it can be written as c - δ_q for some superstable config c.

def maximal_superstable (G : CFGraph) {q : G.V} (c : Config G q) : Prop

A maximal superstable configuration has no legal firings and is not ≤ any other superstable configuration.

Equations

• maximal_superstable G c = (superstable G q c ∧ ∀ (c' : Config G q), superstable G q c' → c ≤ c' → c' = c)

theorem helper_superstable_to_unwinnable {G : CFGraph} (h_conn : graph_connected G) (q : G.V) (c : Config G q) : maximal_superstable G c → ¬winnable G (c.vertex_degree - one_chip q)

Subtracting a chip at q from a superstable configuration gives an unwinnable divisor.

Burn lists and Dhar's burning algorithm

A burn list for a configuration c is an ordered list of distinct vertices ending at q. The list is stored in reverse burn order: starting from [q], each new burnable vertex is prepended to the list. A vertex is burnable when its number of chips is less than its out-degree into the vertices that have already burned. The key property is that a configuration is superstable if and only if a complete burn list, one containing all vertices, exists (superstable_burn_list).

The burn_flow function extracts an orientation from a burn list by directing each edge toward the vertex that appears earlier in the list. This is used to construct the bijection between maximal superstable configurations and acyclic orientations with unique source q (see Orientation.lean).

def is_burn_list (G : CFGraph) {q : G.V} (c : Config G q) (L : List G.V) : Prop

Definition: A burn list for a configuration c is a list [v_1, v_2, ..., v_n, q] of distinct vertices ending at q, stored in reverse burn order. For each i, let S_i = G.V \ {v_{i+1}, ..., v_n, q}. Then v_i ∈ S_i, and the out-degree of v_i with respect to S_i, i.e. the number of edges from v_i to the later vertices {v_{i+1}, ..., v_n, q}, is greater than the number of chips at v_i.

Equations

• is_burn_list G c [] = False
• is_burn_list G c [x] = (x = q)
• is_burn_list G c (v :: w :: rest) = (outdeg_S G q (Finset.univ \ (w :: rest).toFinset) v > c.vertex_degree v ∧ ¬(w :: rest).contains v = true ∧ is_burn_list G c (w :: rest))

structure burn_list (G : CFGraph) {q : G.V} (c : Config G q) : Type u_1

A bundled burn list: a list L of vertices together with a proof that it satisfies the is_burn_list conditions for configuration c.

• list : List G.V
• h_burn_list : is_burn_list G c self.list

theorem superstable_burn_list (G : CFGraph) {q : G.V} (c : Config G q) (h_ss : superstable G q c) : ∃ (L : burn_list G c), ∀ (v : G.V), v ∈ L.list

A superstable configuration admits a complete burn list containing every vertex of G. This is the key output of Dhar's burning algorithm: in a superstable configuration, the whole graph burns.

def burn_flow {G : CFGraph} {q : G.V} {c : Config G q} (L : burn_list G c) : G.V × G.V → ℕ

The orientation induced by a burn list: for each edge (u, v), direct it from u to v (i.e. assign nonzero flow) if u appears in the list and v appears before u. In other words, the orientation indicates the direction of the spreading fire in Dhar's burning algorithm.

Equations

• burn_flow L e = if e.1 ∈ L.list ∧ List.idxOf e.2 L.list < List.idxOf e.1 L.list then num_edges G e.1 e.2 else 0

theorem burn_flow_reverse {G : CFGraph} {q : G.V} {c : Config G q} (L : burn_list G c) (h_full : ∀ (v : G.V), v ∈ L.list) (u v : G.V) : burn_flow L (u, v) + burn_flow L (v, u) = num_edges G u v

The burn_flow of a complete burn list is a valid orientation: for every edge {u, v}, exactly num_edges G u v units of flow are directed in one of the two directions.

theorem burn_flow_directed {G : CFGraph} {q : G.V} {c : Config G q} (L : burn_list G c) (h_full : ∀ (v : G.V), v ∈ L.list) (u v : G.V) : burn_flow L (u, v) = 0 ∨ burn_flow L (v, u) = 0

The burn_flow of a complete burn list is directed: for every pair (u, v), flow goes in at most one direction.

@[irreducible]

theorem burnin_degree {G : CFGraph} {q : G.V} {c : Config G q} (L : burn_list G c) (v : G.V) (h_pres : v ∈ L.list) (h_ne : v ≠ q) : ↑(∑ w : G.V, burn_flow L (w, v)) > c.vertex_degree v

For any non-q vertex v in a burn list, the in-flow into v exceeds the number of chips at v. This is the key inequality used to construct the acyclic orientation from a maximal superstable configuration.