ChipFiringConfiguration

Configurations and superstable configurations

Fix a vertex $q \in V(G)$. A configuration (ChipFiringConfiguration 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 outdegreeSet G 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$: $\widetilde V = V(G) \setminus \{q\}$.

Equations

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

structure ChipFiringConfiguration (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 configDegree {G : CFGraph} {q : G.V} (c : ChipFiringConfiguration 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

• configDegree c = CFDiv.degree c.chips

def toDiv {G : CFGraph} {q : G.V} (d : ℤ) (c : ChipFiringConfiguration 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.chips + (d - configDegree c) • oneChip q

theorem ChipFiringConfiguration.ext {G : CFGraph} {q : G.V} {c₁ c₂ : ChipFiringConfiguration 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 ChipFiringConfiguration.ext_iff {G : CFGraph} {q : G.V} {c₁ c₂ : ChipFiringConfiguration G q} : c₁ = c₂ ↔ ∀ (v : G.V), c₁.chips v = c₂.chips v

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

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₂ : ChipFiringConfiguration 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 toQEffectiveDivisor {G : CFGraph} {q : G.V} (d : ℤ) (c : ChipFiringConfiguration G q) : qEffectiveDivisor G q

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

Equations

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

def toConfig {G : CFGraph} {q : G.V} (D : qEffectiveDivisor G q) : ChipFiringConfiguration G q

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

Equations

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

theorem config_degree_div_degree {G : CFGraph} {q : G.V} (D : qEffectiveDivisor G q) : CFDiv.degree 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 toDiv_config_degree_add {G : CFGraph} {q : G.V} (c : ChipFiringConfiguration 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 deg_chips_sub_one_chip {G : CFGraph} {q : G.V} (c : ChipFiringConfiguration G q) : CFDiv.degree (c.chips - oneChip q) = configDegree c - 1

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

theorem div_of_config_of_div {G : CFGraph} {q : G.V} (D : qEffectiveDivisor G q) : toDiv (CFDiv.degree D.D) (toConfig D) = D.D

toQEffectiveDivisor 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 : qReduced G q D) : toDiv (CFDiv.degree 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_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 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 config_eff {G : CFGraph} {q : G.V} (d : ℤ) (c : ChipFiringConfiguration 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 instPartialOrderChipFiringConfiguration {G : CFGraph} {q : G.V} : PartialOrder (ChipFiringConfiguration G q)

Equations

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

theorem config_degree_mono {G : CFGraph} {q : G.V} {c c' : ChipFiringConfiguration 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 config_eq_of_le_and_degree {G : CFGraph} {q : G.V} {c1 c2 : ChipFiringConfiguration 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 superstable (G : CFGraph) (q : G.V) (c : ChipFiringConfiguration 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.chips v < outdegreeSet G S v

theorem superstable_iff_q_reduced (G : CFGraph) (q : G.V) (d : ℤ) (c : ChipFiringConfiguration 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, Remark 3.14.

theorem 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 q_reduced_superstable_correspondence (G : CFGraph) (q : G.V) (D : CFDiv G) : qReduced G q D ↔ ∃ (c : ChipFiringConfiguration G q), superstable G q c ∧ D = toDiv (CFDiv.degree D) c

A divisor is $q$-reduced if and only if it corresponds to a superstable configuration with respect to $q$.

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

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

Equations

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

theorem superstable_sub_chip_unwinnable {G : CFGraph} (q : G.V) (c : ChipFiringConfiguration 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 isBurnList (G : CFGraph) {q : G.V} (c : ChipFiringConfiguration 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

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

structure burnList (G : CFGraph) {q : G.V} (c : ChipFiringConfiguration 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

  The ordered vertices satisfying the burning-list conditions for the configuration.

• h_burn_list : isBurnList G c self.list

theorem superstable_burn_list (G : CFGraph) {q : G.V} (c : ChipFiringConfiguration 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 burnFlow {G : CFGraph} {q : G.V} {c : ChipFiringConfiguration 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

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

theorem burn_flow_reverse {G : CFGraph} {q : G.V} {c : ChipFiringConfiguration 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 burn_flow_directed {G : CFGraph} {q : G.V} {c : ChipFiringConfiguration 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 burnin_degree {G : CFGraph} {q : G.V} {c : ChipFiringConfiguration 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.