Chip-firing graphs

A chip-firing graph (CFGraph) is a loopless undirected multigraph with bundled vertex type G.V (assumed Fintype, DecidableEq, and Nonempty). Edges are stored as a multiset of pairs; num_edges G v w counts total edge multiplicity between v and w, including both (v, w) and (w, v) entries.

We define the degree (valence) of a vertex as the sum of edge multiplicities at that vertex, and the genus (cyclomatic number) g = |E| - |G.V| + 1, which plays a central role in the Riemann-Roch theorem for graphs ([Corry-Perkinson], Chapter 5).

Many main theorems in this library require connectivity; see graph_connected. In those cases, a proof of connectivity must be provided as an additional argument.

structure CFGraph : Type (u + 1)

A chip-firing graph is a loopless multigraph. It is not assumed connected by default, though many of our main theorems pertain to connected graphs.

• V : Type u
• instDecidableEq : DecidableEq self.V
• instFintype : Fintype self.V
• instNonempty : Nonempty self.V
• edges : Multiset (self.V × self.V)
• loopless (v : self.V) : (v, v) ∉ self.edges

def num_edges (G : CFGraph) (v w : G.V) : ℕ

The number of edges between vertex v and vertex w. When working with chip-firing graphs in this repository, it is usually preferable to work with this function, rather than with the multiset of edges directly.

Equations

• num_edges G v w = (Multiset.filter (fun (e : G.V × G.V) => e = (v, w) ∨ e = (w, v)) G.edges).card

def graph_connected (G : CFGraph) : Prop

A graph is connected if the vertices cannot be partitioned into two nonempty sets with no edges between them. This is equivalent to saying there is a path between any two vertices, but the first definition is more convenient to work with in this repository.

Equations

• graph_connected G = ∀ (S : Finset G.V), (∃ (v : G.V) (w : G.V), v ∈ S ∧ w ∉ S) → ∃ v ∈ S, ∃ w ∉ S, num_edges G v w > 0

def genus (G : CFGraph) : ℤ

The genus of a graph is its cyclomatic number: |E| - |G.V| + 1.

Equations

• genus G = ↑G.edges.card - ↑(Fintype.card G.V) + 1

theorem num_edges_symmetric (G : CFGraph) (v w : G.V) : num_edges G v w = num_edges G w v

Number of edges is symmetric

@[simp]

theorem num_edges_self_zero (G : CFGraph) (v : G.V) : num_edges G v v = 0

Numerical version of loopless: num_edges v v = 0.

def vertex_degree (G : CFGraph) (v : G.V) : ℤ

Degree (valence) of a vertex as an integer (defined as the sum of incident edge multiplicities)

Equations

• vertex_degree G v = ∑ u : G.V, ↑(num_edges G v u)

The divisor group

A divisor (CFDiv G) is an integer-valued function on the vertices of a chip-firing graph, representing a distribution of chips (possibly negative, i.e. debt) across vertices. The divisor group Div(G) = CFDiv G is the abelian group G.V → ℤ under pointwise addition. ([Corry-Perkinson], Definition 1.3)

This section establishes basic operations on divisors: pointwise arithmetic lemmas, the firing move at a single vertex (lending chips to all neighbors), the borrowing move (the inverse operation), and the generalization to set firing ([Corry-Perkinson], Definitions 1.5–1.6). The firing vector firing_vector G v is the principal divisor produced by firing vertex v once.

@[reducible, inline]

abbrev CFDiv (G : CFGraph) : Type u_1

A divisor is a function from vertices to integers. [Corry-Perkinson], Definition 1.3

Equations

• CFDiv G = (G.V → ℤ)

def one_chip {G : CFGraph} (v_chip : G.V) : CFDiv G

A divisor with one chip at a specified vertex v_chip and zero chips elsewhere.

Equations

• one_chip v_chip v = if v = v_chip then 1 else 0

@[simp]

theorem one_chip_apply_other {G : CFGraph} (v w : G.V) : v ≠ w → one_chip v w = 0

@[simp]

theorem add_apply {G : CFGraph} (D₁ D₂ : CFDiv G) (v : G.V) : (D₁ + D₂) v = D₁ v + D₂ v

@[simp]

theorem sub_apply {G : CFGraph} (D₁ D₂ : CFDiv G) (v : G.V) : (D₁ - D₂) v = D₁ v - D₂ v

@[simp]

theorem smul_apply {G : CFGraph} (n : ℤ) (D : CFDiv G) (v : G.V) : (n • D) v = n * D v

def firing_move (G : CFGraph) (D : CFDiv G) (v : G.V) : CFDiv G

Firing move at a vertex [Corry-Perkinson], Definition 1.5

Equations

• firing_move G D v w = if w = v then D v - vertex_degree G v else D w + ↑(num_edges G v w)

def borrowing_move (G : CFGraph) (D : CFDiv G) (v : G.V) : CFDiv G

Borrowing move at a vertex

Equations

• borrowing_move G D v w = if w = v then D v + vertex_degree G v else D w - ↑(num_edges G v w)

def set_firing (G : CFGraph) (D : CFDiv G) (S : Finset G.V) : CFDiv G

Result of firing a set S on a vertex D [Corry-Perkinson], Definition 1.6

Equations

• set_firing G D S w = D w + ∑ v ∈ S, if w = v then -vertex_degree G v else ↑(num_edges G v w)

def firing_vector (G : CFGraph) (v : G.V) : CFDiv G

The principal divisor associated to firing a single vertex

Equations

• firing_vector G v w = if w = v then -vertex_degree G v else ↑(num_edges G v w)

def set_firing_vector (G : CFGraph) (D : CFDiv G) (S : Finset G.V) : CFDiv G

The firing vector for a set of vertices

Equations

• set_firing_vector G D S w = ∑ v ∈ S, if w = v then -vertex_degree G v else ↑(num_edges G v w)

Principal divisors and linear equivalence

A firing script (firing_script G = G.V → ℤ) assigns an integer firing level to each vertex. The associated principal divisor prin G σ records the net chip flow at each vertex when script σ is applied: (prin G σ)(v) = Σ_u (σ(u) - σ(v)) · num_edges(v, u) ([Corry-Perkinson], Definition 2.3).

The subgroup of principal divisors principal_divisors G is generated by the firing vectors firing_vector G v for all v. Two divisors D and D' are linearly equivalent (linear_equiv G D D') if their difference is a principal divisor ([Corry-Perkinson], Definition 1.8). This defines an equivalence relation on Div(G), and linearly equivalent divisors have the same degree (see linear_equiv_preserves_deg).

def principal_divisors (G : CFGraph) : AddSubgroup (CFDiv G)

The subgroup of principal divisors is generated by firing vectors at individual vertices.

Equations

• principal_divisors G = AddSubgroup.closure (Set.range (firing_vector G))

def linear_equiv (G : CFGraph) (D D' : CFDiv G) : Prop

Two divisors are linearly equivalent if their difference is a principal divisor. [Corry-Perkinson], Definition 1.8

Equations

• linear_equiv G D D' = (D' - D ∈ principal_divisors G)

theorem linear_equiv_is_equivalence (G : CFGraph) : Equivalence (linear_equiv G)

Linear equivalence is an equivalence relation on Div(G).

@[reducible, inline]

abbrev firing_script (G : CFGraph) : Type u_1

A firing script is an integer-valued function on vertices, recording how many times each vertex is fired. Negative values represent borrowing. [Corry-Perkinson], Definition 2.2

Equations

• firing_script G = (G.V → ℤ)

def prin (G : CFGraph) : firing_script G →+ CFDiv G

The group homomorphism sending a firing script σ to the principal divisor (prin G σ)(v) = Σ_u (σ(u) - σ(v)) * num_edges G v u. [Corry-Perkinson], Definition 2.3 (denoted div(σ) there)

Equations

• prin G = { toFun := fun (σ : firing_script G) (v : G.V) => ∑ u : G.V, (σ u - σ v) * ↑(num_edges G v u), map_zero' := ⋯, map_add' := ⋯ }

theorem principal_iff_eq_prin (G : CFGraph) (D : CFDiv G) : D ∈ principal_divisors G ↔ ∃ (σ : firing_script G), D = (prin G) σ

A divisor is principal if and only if it equals prin G σ for some firing script σ. This gives a concrete characterization of the subgroup principal_divisors G.

Effective divisors and winnability

A divisor is effective if it assigns a nonnegative number of chips to every vertex ([Corry-Perkinson], Definition 1.13). The divisor group carries a natural partial order where D₁ ≤ D₂ iff D₁ v ≤ D₂ v for all v; effectivity is equivalent to D ≥ 0. The submonoid of effective divisors is denoted Eff G.

A divisor D is winnable if it is linearly equivalent to some effective divisor ([Corry-Perkinson], Definition 1.14) — that is, the players can collectively win the dollar game starting from position D.

def effective {G : CFGraph} (D : CFDiv G) : Prop

A divisor is effective if it assigns a nonnegative integer to every vertex. Equivalently, it is ≥ 0. [Corry-Perkinson], Definition 1.13

Equations

• effective D = ∀ (v : G.V), D v ≥ 0

def Eff (G : CFGraph) : AddSubmonoid (CFDiv G)

The submonoid of effective divisors is denoted Eff G.

Equations

• Eff G = { carrier := {D : CFDiv G | effective D}, add_mem' := ⋯, zero_mem' := ⋯ }

def eff_one_chip {G : CFGraph} (v : G.V) : effective (one_chip v)

A one-chip divisor is effective.

Equations

• ⋯ = ⋯

theorem sub_eff_iff_geq {G : CFGraph} (D₁ D₂ : CFDiv G) : effective (D₁ - D₂) ↔ D₁ ≥ D₂

D₁ - D₂ is effective iff D₁ ≥ D₂.

def winnable (G : CFGraph) (D : CFDiv G) : Prop

A divisor is winnable if it is linearly equivalent to an effective divisor. [Corry-Perkinson], Definition 1.14

Equations

• winnable G D = ∃ D' ∈ Eff G, linear_equiv G D D'

The degree homomorphism and the Laplacian

The degree of a divisor D is $\deg(D) = \sum_v D(v)$, the total number of chips ([Corry-Perkinson], Definition 1.4). It is a group homomorphism $\mathrm{Div}(G) \to \mathbb{Z}$. Principal divisors have degree zero, so linearly equivalent divisors have equal degree ([Corry-Perkinson], Proposition 1.15).

The Laplacian matrix laplacian_matrix G is the matrix $L = \mathrm{Deg}(G) - A$, where $\mathrm{Deg}(G)$ is the diagonal degree matrix and $A$ is the adjacency matrix ([Corry-Perkinson], Definition 2.6). Applying the Laplacian to a firing script produces the corresponding principal divisor.

def deg {G : CFGraph} : CFDiv G →+ ℤ

Degree of a divisor is the sum of its values at all vertices. [Corry-Perkinson], Definition 1.4

Equations

• deg = { toFun := fun (D : CFDiv G) => ∑ v : G.V, D v, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem deg_one_chip {G : CFGraph} (v : G.V) : deg (one_chip v) = 1

theorem deg_of_eff_nonneg {G : CFGraph} (D : CFDiv G) : effective D → deg D ≥ 0

Effective divisors have nonnegative degree.

theorem eff_degree_zero {G : CFGraph} (D : CFDiv G) : effective D → deg D = 0 → D = 0

The only effective divisor of degree 0 is 0.

theorem linear_equiv_preserves_deg (G : CFGraph) (D D' : CFDiv G) (h_equiv : linear_equiv G D D') : deg D = deg D'

Linearly equivalent divisors have the same degree. [Corry-Perkinson], Proposition 1.15

theorem helper_divisor_decomposition (G : CFGraph) (E'' : CFDiv G) (k₁ k₂ : ℕ) (h_effective : effective E'') (h_deg : deg E'' = ↑k₁ + ↑k₂) : ∃ (E₁ : CFDiv G) (E₂ : CFDiv G), effective E₁ ∧ effective E₂ ∧ deg E₁ = ↑k₁ ∧ deg E₂ = ↑k₂ ∧ E'' = E₁ + E₂

An effective divisor of degree k₁ + k₂ can be decomposed into a sum of two effective divisors of degrees k₁ and k₂ respectively.

def laplacian_matrix (G : CFGraph) : Matrix G.V G.V ℤ

The Laplacian matrix of a CFGraph. [Corry-Perkinson], Definition 2.6

Equations

• laplacian_matrix G i j = if i = j then vertex_degree G i else -↑(num_edges G i j)

def apply_laplacian (G : CFGraph) (σ : firing_script G) (D : CFDiv G) : CFDiv G

Apply the Laplacian matrix to a firing script, and current divisor to get a new divisor.

Equations

• apply_laplacian G σ D v = D v - (laplacian_matrix G).mulVec σ v

q-effective divisors

Fix a vertex $q$. A divisor $D$ is $q$-effective if $D(v) \geq 0$ for all $v \neq q$; it may have an arbitrary (possibly negative) value at $q$ itself. The structure q_eff_div packages such a divisor with its proof of $q$-effectivity.

A key fact for connected graphs is that every divisor is linearly equivalent to a $q$-effective divisor (q_effective_exists). The proof goes via the notion of a benevolent set: a set $S$ is benevolent if any divisor can be made to have all its debt concentrated on $S$ via firing moves.

def q_effective {G : CFGraph} (q : G.V) (D : CFDiv G) : Prop

Call a divisor q-effective if it has a nonnegative number of chips at all vertices except possibly q.

Equations

• q_effective q D = ∀ (v : G.V), v ≠ q → D v ≥ 0

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

A divisor that is q-effective.

• D : CFDiv G
• h_eff : q_effective q self.D

def benevolent (G : CFGraph) (S : Finset G.V) : Prop

A set of vertices is benevolent if it is possible to concentrate all debt on this set.

Equations

• benevolent G S = ∀ (D : CFDiv G), ∃ (E : CFDiv G), linear_equiv G D E ∧ ∀ (v : G.V), E v < 0 → v ∈ S

theorem q_effective_exists {G : CFGraph} (h_conn : graph_connected G) (q : G.V) (D : CFDiv G) : ∃ (E : CFDiv G), q_effective q E ∧ linear_equiv G D E

Every divisor can have its debt concentrated on on vertex, as long as the graph is connected. That is, D is linearly equivalent to a q-effective divisor.

The q-reduction partial order

A firing script $\sigma$ is a $q$-reducer if $\sigma(q) \leq \sigma(v)$ for all $v$, meaning $q$ is fired the least (or not at all relative to the others). The relation reduces_to G q D₁ D₂ holds when $D_2$ is obtained from $D_1$ by applying a $q$-reducer script, i.e. $D_2 = D_1 + \mathrm{prin}(\sigma)$ for some $q$-reducer $\sigma$.

This relation is reflexive and transitive, and in connected graphs it is also antisymmetric (reduces_to_antisymmetric), making it a partial order on $q$-effective divisors. The antisymmetry relies on the fact that a firing script with trivial principal divisor must be constant (constant_script_of_zero_prin).

def q_reducer (G : CFGraph) (q : G.V) (σ : firing_script G) : Prop

A firing script σ is a $q$-reducer if q is fired the minimum number of times: σ q ≤ σ v for all v.

Equations

• q_reducer G q σ = ∀ (v : G.V), σ q ≤ σ v

def reduces_to (G : CFGraph) (q : G.V) (D₁ D₂ : CFDiv G) : Prop

reduces_to G q D₁ D₂ holds when D₂ is obtained from D₁ by applying a $q$-reducer script: D₂ = D₁ + prin G σ for some σ with σ q ≤ σ v for all v.

Equations

• reduces_to G q D₁ D₂ = ∃ (σ : firing_script G), q_reducer G q σ ∧ D₂ = D₁ + (prin G) σ

q-reduced divisors

A $q$-effective divisor $D$ is $q$-reduced if, for every nonempty set $S \subseteq G.V \setminus \{q\}$, some vertex in $S$ would go into debt if $S$ were fired ([Corry-Perkinson], Definition 3.4). Equivalently, $D$ is the maximum element of its linear equivalence class in the $q$-reduction partial order.

The main results of this section are:

• Every divisor has a unique $q$-reduced representative (exists_q_reduced_representative, q_reduced_unique), corresponding to [Corry-Perkinson], Theorem 3.6.
• A divisor is winnable if and only if its $q$-reduced representative is effective (winnable_iff_q_reduced_effective), corresponding to [Corry-Perkinson], Corollary 3.7.

The existence proof proceeds by defining an active vertex (one that can still be fired while maintaining $q$-effectivity) and showing that the reduction_excess — the total chips at active vertices — strictly decreases at each reduction step.

def q_reduced (G : CFGraph) (q : G.V) (D : CFDiv G) : Prop

A divisior is q-reduced if it is effective away from q, but firing any vertex set disjoint from q puts some vertex into debt. [Corry-Perkinson], Definition 3.4

Equations

• q_reduced G q D = (q_effective q D ∧ ∀ S ⊆ {x : G.V | x ≠ q}, S.Nonempty → ∃ v ∈ S, D v < ∑ w : G.V with w ∉ S, ↑(num_edges G v w))

theorem effective_of_winnable_and_q_reduced (G : CFGraph) (q : G.V) (D : CFDiv G) : winnable G D → q_reduced G q D → effective D

A winnable $q$-reduced divisor is effective.

theorem q_reduced_unique (G : CFGraph) (q : G.V) (D₁ D₂ : CFDiv G) : q_reduced G q D₁ ∧ q_reduced G q D₂ ∧ linear_equiv G D₁ D₂ → D₁ = D₂

The q-reduced representative of a divisor class is unique. [Corry-Perkinson], Theorem 3.6, part 2 (uniqueness).

def active (G : CFGraph) (q : G.V) (D : CFDiv G) (v : G.V) : Prop

A vertex is called ``active'' if there exists a firing script that leaves the divisor effective away from q, does not fire q, and fires at least once at that vertex.

Equations

• active G q D v = ∃ (σ : firing_script G), q_reducer G q σ ∧ q_effective q (D + (prin G) σ) ∧ σ q < σ v

noncomputable def reduction_excess (G : CFGraph) (q : G.V) (D : CFDiv G) : ℤ

The total chips held at active vertices of D. This quantity strictly decreases at each step of the $q$-reduction algorithm, providing the termination measure for q_effective_to_q_reduced.

Equations

• reduction_excess G q D = ∑ v : G.V, if active G q D v then D v else 0

@[irreducible]

theorem q_effective_to_q_reduced {G : CFGraph} (h_conn : graph_connected G) {q : G.V} {D : CFDiv G} (h_eff : q_effective q D) : ∃ (E : CFDiv G), q_reduced G q E ∧ linear_equiv G D E

In a connected graph, every $q$-effective divisor is linearly equivalent to a $q$-reduced divisor. The proof is by induction on reduction_excess.

theorem exists_q_reduced_representative {G : CFGraph} (h_conn : graph_connected G) (q : G.V) (D : CFDiv G) : ∃ (D' : CFDiv G), linear_equiv G D D' ∧ q_reduced G q D'

Every divisor is linearly equivalent to some $q$-reduced divisor. [Corry-Perkinson], Theorem 3.6, part 1 (existence).

theorem unique_q_reduced {G : CFGraph} (h_conn : graph_connected G) (q : G.V) (D : CFDiv G) : ∃! D' : CFDiv G, linear_equiv G D D' ∧ q_reduced G q D'

Every divisor is linearly equivalent to exactly one $q$-reduced divisor. [Corry-Perkinson], Theorem 3.6 (existence and uniqueness combined).

theorem winnable_iff_q_reduced_effective {G : CFGraph} (h_conn : graph_connected G) (q : G.V) (D : CFDiv G) : winnable G D ↔ ∃ (D' : CFDiv G), linear_equiv G D D' ∧ q_reduced G q D' ∧ effective D'

A divisor is winnable if and only if its q-reduced representative is effective. [Corry-Perkinson], Corollary 3.7, rephrased.