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 quantity outdegS G S v counts edges from $v$ to vertices outside $S$, and is the relevant threshold for the superstability condition.

@[reducible, inline]

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

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

Equations

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

structure ChipFiring.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.

• chips : CFDiv G

  The divisor recording the chip count at each vertex.

• q_zero : self.chips q = 0

  The distinguished vertex $q$ has no chips.

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

  All chip counts are nonnegative.

def ChipFiring.configDegree {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

• ChipFiring.configDegree c = ChipFiring.deg c.chips

def ChipFiring.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

• ChipFiring.toDiv d c = c.chips + (d - ChipFiring.configDegree c) • ChipFiring.oneChip q

theorem ChipFiring.Config.ext {G : CFGraph} {q : G.V} {c₁ c₂ : Config G q} (h : ∀ (v : G.V), c₁.chips v = c₂.chips v) : c₁ = c₂

Two configurations are equal if their chip counts agree at every vertex.

theorem ChipFiring.Config.ext_iff {G : CFGraph} {q : G.V} {c₁ c₂ : Config G q} : c₁ = c₂ ↔ ∀ (v : G.V), c₁.chips v = c₂.chips v

theorem ChipFiring.eq_config_iff_eq_chips {G : CFGraph} {q : G.V} (c₁ c₂ : Config G q) : c₁ = c₂ ↔ c₁.chips = c₂.chips

Two configurations are equal if and only if their underlying divisors agree.

theorem ChipFiring.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 ChipFiring.toQed {G : CFGraph} {q : G.V} (d : ℤ) (c : Config G q) : qEffDiv G q

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

Equations

• ChipFiring.toQed d c = { D := ChipFiring.toDiv d c, h_eff := ⋯ }

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

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

Equations

• ChipFiring.toConfig D = { chips := D.D - D.D q • ChipFiring.oneChip q, q_zero := ⋯, non_negative := ⋯ }

theorem ChipFiring.config_degree_div_degree {G : CFGraph} {q : G.V} (D : qEffDiv G q) : deg D.D = D.D q + configDegree (toConfig D)

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

@[simp]

theorem ChipFiring.toDiv_config_degree_add {G : CFGraph} {q : G.V} (c : Config G q) (k : ℤ) : toDiv (configDegree c + k) c = c.chips + k • oneChip q

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

@[simp]

theorem ChipFiring.deg_chips_sub_one_chip {G : CFGraph} {q : G.V} (c : Config G q) : deg (c.chips - oneChip q) = configDegree c - 1

The divisor $c-q$ has degree $\deg(c)-1$.

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

toQed 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 ChipFiring.q_reduced_toDiv_toConfig (G : CFGraph) (q : G.V) (D : CFDiv G) (h_qred : qReduced 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 ChipFiring.q_reduced_eq_chips_add_q (G : CFGraph) (q : G.V) (D : CFDiv G) (h_qred : qReduced G q D) : D = (toConfig { D := D, h_eff := ⋯ }).chips + D q • oneChip q

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

theorem ChipFiring.q_reduced_eq_chips_sub_one_chip (G : CFGraph) (q : G.V) (D : CFDiv G) (h_qred : qReduced G q D) (h_q : D q = -1) : D = (toConfig { D := D, h_eff := ⋯ }).chips - oneChip q

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

theorem ChipFiring.config_eff {G : CFGraph} {q : G.V} (d : ℤ) (c : Config G q) : effective (toDiv d c) ↔ d ≥ configDegree 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.

@[instance_reducible]

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

Equations

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

theorem ChipFiring.config_degree_mono {G : CFGraph} {q : G.V} {c c' : Config G q} (h_le : c ≤ c') : configDegree c ≤ configDegree c'

The configuration degree is monotone: if $c \le c'$ pointwise, then $\deg(c) \le \deg(c')$.

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

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

def ChipFiring.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, preliminary version, Definition 3.13.

Equations

• ChipFiring.superstable G q c = ∀ S ⊆ ChipFiring.Vtilde q, S.Nonempty → ∃ v ∈ S, c.chips v < ChipFiring.outdegS G S v

theorem ChipFiring.superstable_iff_q_reduced (G : CFGraph) (q : G.V) (d : ℤ) (c : Config G q) : superstable G q c ↔ qReduced 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, preliminary version, Remark 3.15.

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

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

theorem ChipFiring.q_reduced_superstable_correspondence (G : CFGraph) (q : G.V) (D : CFDiv G) : qReduced 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 corresponds to a superstable configuration with respect to $q$.

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

A maximal superstable configuration is not strictly dominated by any other superstable configuration.

Equations

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

theorem ChipFiring.superstable_sub_chip_unwinnable {G : CFGraph} (q : G.V) (c : Config G q) : superstable G q c → ¬winnable G (c.chips - oneChip 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 burnFlow 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 ChipFiring.isBurnList (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

• ChipFiring.isBurnList G c [] = False
• ChipFiring.isBurnList G c [x] = (x = q)
• ChipFiring.isBurnList G c (v :: w :: rest) = (ChipFiring.outdegS G (Finset.univ \ (w :: rest).toFinset) v > c.chips v ∧ ¬(w :: rest).contains v = true ∧ ChipFiring.isBurnList G c (w :: rest))

structure ChipFiring.burnList (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 isBurnList conditions for configuration $c$.

• list : List G.V

  Ordered list of vertices satisfying the burning condition.

• h_burn_list : isBurnList G c self.list

theorem ChipFiring.superstable_burn_list (G : CFGraph) {q : G.V} (c : Config G q) (h_ss : superstable G q c) : ∃ (L : burnList 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 ChipFiring.burnFlow {G : CFGraph} {q : G.V} {c : Config G q} (L : burnList 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

• ChipFiring.burnFlow L e = if e.1 ∈ L.list ∧ List.idxOf e.2 L.list < List.idxOf e.1 L.list then ChipFiring.numEdges G e.1 e.2 else 0

theorem ChipFiring.burn_flow_reverse {G : CFGraph} {q : G.V} {c : Config G q} (L : burnList G c) (h_full : ∀ (v : G.V), v ∈ L.list) (u v : G.V) : burnFlow L (u, v) + burnFlow L (v, u) = numEdges G u v

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

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

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

theorem ChipFiring.burnin_degree {G : CFGraph} {q : G.V} {c : Config G q} (L : burnList G c) (v : G.V) (h_pres : v ∈ L.list) (h_ne : v ≠ q) : ↑(∑ w : G.V, burnFlow L (w, v)) > c.chips 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 an acyclic orientation from a superstable configuration.