Chip-firing graphs

A chip-firing graph (CFGraph) is a loopless undirected multigraph with bundled vertex type $V(G)$, implemented as G.V and assumed to be finite, decidably equal, and nonempty. Edges are stored as a multiset of ordered pairs; num_edges G v w counts the 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| - |V(G)| + 1$, which plays a central role in the Riemann-Roch theorem for graphs.

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 edge multiplicity between vertices $v$ and $w$.

When working with chip-firing graphs in this repository, prefer this function to the underlying multiset of edges.

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 its vertices cannot be partitioned into two nonempty sets with no edges between them.

This is equivalent to saying that there is a path between any two vertices, but the partition formulation is more convenient 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| - |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

The number of edges between two vertices is symmetric (the graph is undirected).

@[simp]

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

Numerical version of loopless: the number of edges from a vertex to itself is zero.

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

The degree, or valence, of a vertex as an integer.

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 $\operatorname{Div}(G)$ is implemented as CFDiv G, the abelian group of functions $V(G) \to \mathbb{Z}$ under pointwise addition.

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. The firing vector firing_vector G v is the principal divisor produced by firing vertex $v$ once.

See:

• Corry-Perkinson, Definition 1.3.
• Corry-Perkinson, Definitions 1.5-1.6.

@[reducible, inline]

abbrev CFDiv (G : CFGraph) : Type u_1

A divisor is a function from vertices to integers.

See: Corry-Perkinson, Definition 1.3.

Equations

• CFDiv G = (G.V → ℤ)

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

The divisor with one chip at a specified vertex $v_{\mathrm{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

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

The result of firing a vertex $v$, starting from the divisor $D$.

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

The result of borrowing at a vertex $v$, starting from a divisor $D$.

See: Corry-Perkinson, Definition 1.5.

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

The result of firing a set $S$ of vertices, starting from a divisor $D$.

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

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 the script $\sigma$ is applied: $$ (\operatorname{prin}_G \sigma)(v) = \sum_u (\sigma(u)-\sigma(v)) \operatorname{num\_edges}_G(v,u). $$

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. This defines an equivalence relation on $\operatorname{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.

See: Corry-Perkinson, Definition 1.8.

Equations

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

theorem linear_equiv.refl (G : CFGraph) (D : CFDiv G) : linear_equiv G D D

Linear equivalence is reflexive.

theorem linear_equiv.symm {G : CFGraph} {D D' : CFDiv G} : linear_equiv G D D' → linear_equiv G D' D

Linear equivalence is symmetric.

theorem linear_equiv.trans {G : CFGraph} {D₁ D₂ D₃ : CFDiv G} : linear_equiv G D₁ D₂ → linear_equiv G D₂ D₃ → linear_equiv G D₁ D₃

Linear equivalence is transitive.

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

Linear equivalence is an equivalence relation on $\operatorname{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.

See: 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 $\sigma$ to the principal divisor $$ (\operatorname{prin}_G \sigma)(v) = \sum_u (\sigma(u)-\sigma(v)) \operatorname{num\_edges}_G(v,u). $$

See: Corry-Perkinson, Definition 2.3; prin G σ is the negative of the divisor $\operatorname{div}(\sigma)$ defined there, since they implement a firing script as $D \mapsto D - \operatorname{div}(\sigma)$.

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. The divisor group carries a natural partial order, where $D_1 \le D_2$ if and only if $D_1(v) \le D_2(v)$ for all vertices $v$. Effectivity is equivalent to $D \ge 0$. The submonoid of effective divisors is denoted Eff G.

A divisor $D$ is winnable if it is linearly equivalent to some effective divisor. Equivalently, 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 at least $0$.

See: 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' := ⋯ }

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

A one-chip divisor is effective.

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

The divisor $D_1-D_2$ is effective if and only if $D_1 \ge D_2$.

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

A divisor is winnable if it is linearly equivalent to an effective divisor.

See: 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. It is a group homomorphism $\mathrm{Div}(G) \to \mathbb{Z}$. Principal divisors have degree zero, so linearly equivalent divisors have equal degree.

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. Applying the Laplacian to a firing script produces the corresponding principal divisor.

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

The degree of a divisor is the sum of its values over all vertices.

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

See: Corry-Perkinson, Proposition 1.15.

theorem effective_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_1+k_2$ can be decomposed into a sum of two effective divisors of degrees $k_1$ and $k_2$, respectively.

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

The Laplacian matrix of a CFGraph.

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

Applies the Laplacian matrix to a firing script and a current divisor to obtain 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

A divisor is $q$-effective if it has a nonnegative number of chips at every vertex 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 bundled with a proof that it 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 benevolent_of_nonempty {G : CFGraph} (h_conn : graph_connected G) (S : Finset G.V) (h_nonempty : S.Nonempty) : benevolent G S

In a connected graph, any nonempty set is benevolent.

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

In a connected graph, every divisor is linearly equivalent to a $q$-effective divisor.

Equivalently, every divisor can have all of its debt concentrated at $q$.

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

Two further facts about this order do most of the work in the next section: the number of chips at $q$ is monotone along the order (reduces_to_q_mono), and a script that is a $q$-reducer in both directions has zero principal divisor (prin_eq_zero_of_two_sided_reducer) — a connectivity-free shadow of antisymmetry.

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

A firing script $\sigma$ is a $q$-reducer if $q$ is fired the minimum number of times: $\sigma(q) \le \sigma(v)$ for all vertices $v$.

Equations

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

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

The relation reduces_to G q D₁ D₂ holds when $D_2$ is obtained from $D_1$ by applying a $q$-reducer script: $$ D_2 = D_1 + \operatorname{prin}_G(\sigma) $$ for some $\sigma$ with $\sigma(q) \le \sigma(v)$ for all vertices $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 V(G) \setminus \{q\}$, some vertex in $S$ would go into debt if $S$ were fired. 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).
• A divisor is winnable if and only if its $q$-reduced representative is effective (winnable_iff_q_reduced_effective).

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 divisor is $q$-reduced if it is effective away from $q$, and firing any nonempty set of vertices disjoint from $q$ puts some vertex of that set into debt.

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

See: 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 active if there exists a firing script that leaves the divisor effective away from $q$, fires $q$ minimally, and fires this vertex strictly more than $q$.

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 number of 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

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.

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

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

See: Corry-Perkinson, Corollary 3.7, rephrased.

The handshaking theorem

The classical handshaking theorem for loopless multigraphs: the sum of all vertex degrees is twice the number of edges (sum_vertex_degree_eq_twice_card_edges). The proof double counts vertex-edge incidences, via the general counting lemma sum_card_filter_eq_mul. These facts concern only the graph itself, not its divisor theory; they are collected here for independent use. In this library, the handshaking theorem computes the degree of the canonical divisor (see degree_of_canonical_divisor in Orientation.lean).

theorem sum_card_filter_eq_mul (G : CFGraph) (M : Multiset (G.V × G.V)) (crit : G.V → G.V × G.V → Prop) [(v : G.V) → (e : G.V × G.V) → Decidable (crit v e)] (c : ℕ) (h_count : ∀ e ∈ M, {v : G.V | crit v e}.card = c) : ∑ v : G.V, (Multiset.filter (crit v) M).card = c * M.card

If every element of $M$ matches exactly $c$ vertices under crit, then summing the filtered counts over all vertices gives $c$ times the size of $M$.

theorem sum_vertex_degree_eq_twice_card_edges (G : CFGraph) : ∑ v : G.V, vertex_degree G v = 2 * ↑G.edges.card

Handshaking theorem: In a loopless multigraph $G$, the sum of the degrees of all vertices is twice the number of edges:

$$ \sum_{v \in V(G)} \deg(v) = 2 |E(G)|. $$