Configurations and superstable configurations

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

A configuration $c$ is superstable if for every nonempty $S \subseteq V(G) \setminus \{q\}$, some vertex in $S$ has fewer chips than its out-degree to $V(G) \setminus S$. Equivalently, the associated divisor is $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.

Sources:

• Corry-Perkinson, Definition 2.9.
• Corry-Perkinson, Definition 3.12.

@[reducible, inline]

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

The set of vertices other than $q$: $\widetilde V = V(G) \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 call a nonnegative configuration.

See: Corry-Perkinson, Definition 2.9.

• vertex_degree : CFDiv G

  The divisor representing the chip count at each vertex.

• q_zero : self.vertex_degree q = 0

  The distinguished vertex $q$ has no chips.

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

  All chip counts are nonnegative.

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

The degree of a configuration is the sum of all values away from $q$: $$ \deg(c) = \sum_{v \in V(G)\setminus\{q\}} c(v). $$ Since $c(q)=0$, this is implemented as the degree of the underlying divisor.

Equations

• config_degree c = deg c.vertex_degree

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

Converts a configuration $c$ to a divisor of prescribed degree $d$ by placing $d-\deg(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 if and only if their underlying divisors 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 if and only if their images under toDiv d agree.

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

Converts 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

Converts 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 $\deg(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 if and only if $d \ge \deg(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 a vertex $v$ with respect to a set $S$.

This is the number of edges from $v$ to vertices outside $S$, and is 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 V(G) \setminus \{q\}$, some vertex in $S$ has fewer chips than its out-degree to $V(G) \setminus S$.

See: 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 if and only if toDiv d c is $q$-reduced, for any prescribed degree $d$.

See: 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

A divisor is $q$-reduced if and only if it is obtained from a superstable configuration by prescribing its own degree.

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

A maximal superstable configuration is not strictly dominated by 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 maximal 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

A burn list for a configuration $c$ is a list $[v_1,v_2,\ldots,v_n,q]$ of distinct vertices ending at $q$, stored in reverse burn order.

For each $i$, let $$ S_i = V(G) \setminus \{v_{i+1},\ldots,v_n,q\}. $$ Then $v_i \in S_i$, and the out-degree of $v_i$ with respect to $S_i$, equivalently the number of edges from $v_i$ to the later vertices $\{v_{i+1},\ldots,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 vertex $v \ne q$ 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.