Configurations and superstable configurations

Fix a vertex $q \in V$. A configuration (Config V q) is a nonnegative integer assignment to the vertices $V \setminus \{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 V \setminus \{q\}$, some vertex in $S$ has fewer chips than its out-degree into $V \setminus 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 {V : Type} [DecidableEq V] [Fintype V] (q : V) : Finset V

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

Equations

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

structure Config (V : Type) [DecidableEq V] [Fintype V] [Nonempty V] (q : V) : Type

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 V

  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 : V) : self.vertex_degree v ≥ 0

  Proof that all vertices except q have non-negative values

def config_degree {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {q : V} (c : Config V q) : ℤ

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

Equations

• config_degree c = deg c.vertex_degree

def toDiv {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {q : V} (d : ℤ) (c : Config V q) : CFDiv V

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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {q : V} (c₁ c₂ : Config V 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {q : V} (d : ℤ) (c₁ c₂ : Config V q) : c₁ = c₂ ↔ toDiv d c₁ = toDiv d c₂

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

def to_qed {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {q : V} (d : ℤ) (c : Config V q) : q_eff_div V 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {q : V} (D : q_eff_div V q) : Config V 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {q : V} (D : q_eff_div V 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

• ⋯ = ⋯

theorem config_of_div_of_config {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {q : V} (c : Config V q) (d : ℤ) : toConfig (to_qed d c) = c

toConfig is a left inverse of to_qed: converting a configuration to a $q$-effective divisor and back recovers the original configuration.

theorem qeff_divs_equal {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {q : V} (D1 D2 : q_eff_div V q) : D1 = D2 ↔ D1.D = D2.D

Two $q$-effective divisors are equal iff their underlying divisors agree.

theorem div_of_config_of_div {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {q : V} (D : q_eff_div V 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 eval_toDiv_q {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {q : V} (d : ℤ) (c : Config V q) : toDiv d c q = d - config_degree c

@[simp]

theorem eval_toDiv_ne_q {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {q v : V} (d : ℤ) (c : Config V q) (h_v : v ≠ q) : toDiv d c v = c.vertex_degree v

theorem config_eff {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {q : V} (d : ℤ) (c : Config V 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.

def config_ge {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {q : V} (c c' : Config V q) : Prop

Pointwise partial order on configurations: config_ge c c' iff c(v) ≥ c'(v) for all v.

Equations

• config_ge c c' = ∀ (v : V), c.vertex_degree v ≥ c'.vertex_degree v

theorem config_eq_of_ge_and_degree {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {q : V} {c1 c2 : Config V q} (h_ge : config_ge c1 c2) (h_deg : config_degree c1 = config_degree c2) : c1 = c2

Two configurations are equal if one dominates the other pointwise and they have the same degree.

instance instPartialOrderConfig {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {q : V} : PartialOrder (Config V q)

Equations

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

def outdeg_S {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (q : V) (S : Finset V) (v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (q : V) (c : Config V q) : Prop

A configuration c is superstable if for every nonempty $S \subseteq V \setminus \{q\}$, some vertex in $S$ has fewer chips than its out-degree into $V \setminus 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (q : V) (d : ℤ) (c : Config V 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_superstable_correspondence {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (q : V) (D : CFDiv V) : q_reduced G q D ↔ ∃ (c : Config V 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {q : V} (G : CFGraph V) (c : Config V 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 V q), superstable G q c' → config_ge c' c → c' = c)

theorem smul_one_chip {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (k : ℤ) (v_chip : V) : k • one_chip v_chip = fun (v : V) => if v = v_chip then k else 0

theorem linear_equiv_add_congr_right_local {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D_add : CFDiv V) {D1 D2 : CFDiv V} (h : linear_equiv G D1 D2) : linear_equiv G (D1 + D_add) (D2 + D_add)

Linear equivalence is preserved by adding a fixed divisor on the right.

theorem helper_superstable_to_unwinnable {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (h_conn : graph_connected G) (q : V) (c : Config V 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 all vertices ending at q, built by Dhar's burning algorithm: each vertex is added when its number of chips is less than its out-degree into the remaining (unburned) vertices. The key property is that a configuration is superstable if and only if a complete burn list (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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) {q : V} (c : Config V q) (L : List V) : Prop

Definition: A burn list for a Configuraton c is a list [v_1, v_2, ..., v_n, q] of distinct vertices ending at q, where the following condition holds at each vertex except q (which plays a special role): if S is the set V \ {v_1, ..., v_(n-1)} (which contains v_n), then the out-degree of v_n with respect to S is greater than the number of chips at v_n.

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))

theorem burn_list_contains_q {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) {q : V} (c : Config V q) (L : List V) (h_bl : is_burn_list G c L) : L.contains q = true

Every burn list contains q (since the base case of a burn list is [q]).

theorem extend_burn_list {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) {q : V} (c : Config V q) (h_ss : superstable G q c) (L : List V) : is_burn_list G c L → (∃ (v : V), ¬L.contains v = true) → ∃ w ∉ L.toFinset, is_burn_list G c (w :: L)

If c is superstable and a burn list L does not yet contain all vertices, it can be extended by prepending a new vertex. This corresponds to the next edge burning in Dhar's burning algorithm; superstability implies that the entire graph will burn.

structure burn_list {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) {q : V} (c : Config V q) : Type

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 V
• h_burn_list : is_burn_list G c self.list

theorem burn_list_helper {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) {q : V} (c : Config V q) (h_ss : superstable G q c) (n : ℕ) : n < Finset.univ.card → ∃ (L : List V), L.toFinset.card = n + 1 ∧ is_burn_list G c L

For each n < |V|, there exists a burn list of size n+1. Inductive step for superstable_burn_list.

theorem superstable_burn_list {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) {q : V} (c : Config V q) (h_ss : superstable G q c) : ∃ (L : burn_list G c), ∀ (v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} {q : V} {c : Config V q} (L : burn_list G c) : V × 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} {q : V} {c : Config V q} (L : burn_list G c) (h_full : ∀ (v : V), v ∈ L.list) (u v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} {q : V} {c : Config V q} (L : burn_list G c) (h_full : ∀ (v : V), v ∈ L.list) (u v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} {q : V} {c : Config V q} (L : burn_list G c) (v : V) (h_pres : v ∈ L.list) (h_ne : v ≠ q) : ↑(∑ w : 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.