Chip-firing graphs

A chip-firing graph (CFGraph V) is a loopless undirected multigraph with vertex type 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| - |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.

def isLoopless {V : Type} (edges : Multiset (V × V)) : Prop

An edge set is loopless if it does not contain (v,v).

Equations

• isLoopless edges = ∀ (v : V), (v, v) ∉ edges

structure CFGraph (V : Type) [DecidableEq V] [Fintype V] [Nonempty V] : Type

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.

• edges : Multiset (V × V)
• loopless : isLoopless self.edges

def num_edges {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (v w : 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 : V × V) => e = (v, w) ∨ e = (w, v)) G.edges).card

def graph_connected {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) : 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 V), (∃ (v : V) (w : V), v ∈ S ∧ w ∉ S) → ∃ v ∈ S, ∃ w ∉ S, num_edges G v w > 0

def genus {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) : ℤ

The genus of a graph is its cycle rank: |E| - |V| + 1

Equations

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

theorem num_edges_nonneg {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (v w : V) : num_edges G v w ≥ 0

Number of edges between two vertices is non-negative.

theorem num_edges_symmetric {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (v w : V) : num_edges G v w = num_edges G w v

Number of edges is symmetric

@[simp]

theorem num_edges_self_zero {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (v : V) : num_edges G v v = 0

Numerical version of loopless: num_edges v v = 0.

def vertex_degree {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (v : V) : ℤ

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

Equations

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

theorem vertex_degree_nonneg {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (v : V) : vertex_degree G v ≥ 0

Vertex degree is non-negative

The divisor group

A divisor (CFDiv V) 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 V is the abelian group 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.

def CFDiv (V : Type) : Type

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

Equations

• CFDiv V = (V → ℤ)

instance instAddCommGroupCFDiv {V : Type} : AddCommGroup (CFDiv V)

CFDiv V forms an Additive Commutative Group.

Equations

• instAddCommGroupCFDiv = Pi.addCommGroup

def one_chip {V : Type} [DecidableEq V] (v_chip : V) : CFDiv V

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_v {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (v : V) : one_chip v v = 1

@[simp]

theorem one_chip_apply_other {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (v w : V) : v ≠ w → one_chip v w = 0

@[simp]

theorem one_chip_apply_other' {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (v w : V) : w ≠ v → one_chip v w = 0

@[simp]

theorem add_apply {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (D₁ D₂ : CFDiv V) (v : V) : (D₁ + D₂) v = D₁ v + D₂ v

@[simp]

theorem sub_apply {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (D₁ D₂ : CFDiv V) (v : V) : (D₁ - D₂) v = D₁ v - D₂ v

@[simp]

theorem zero_apply {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (v : V) : 0 v = 0

@[simp]

theorem neg_apply {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (D : CFDiv V) (v : V) : (-D) v = -D v

@[simp]

theorem distrib_sub_add {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (D₁ D₂ D₃ : CFDiv V) : D₁ - (D₂ + D₃) = D₁ - D₂ - D₃

theorem add_sub_distrib {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (D₁ D₂ D₃ : CFDiv V) : D₁ + D₂ - D₃ = D₁ - D₃ + D₂

@[simp]

theorem smul_apply {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (n : ℤ) (D : CFDiv V) (v : V) : (n • D) v = n * D v

def firing_move {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (v : V) : CFDiv V

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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (v : V) : CFDiv V

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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (S : Finset V) : CFDiv V

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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (v : V) : CFDiv V

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)

theorem firing_move_eq_add_firing_vector {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (v : V) : firing_move G D v = D + firing_vector G v

Applying a firing move is equivalent to adding the firing vector.

def set_firing_vector {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (S : Finset V) : CFDiv V

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)

theorem set_firing_eq_add_set_firing_vector {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (S : Finset V) : set_firing G D S = D + set_firing_vector G D S

Set firing equals adding the set firing vector.

Principal divisors and linear equivalence

A firing script (firing_script V = 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) : AddSubgroup (CFDiv V)

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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D D' : CFDiv V) : 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 mem_principal_divisors_firing_vector {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (v : V) : firing_vector G v ∈ principal_divisors G

Lemma: Principal divisors contain the firing vector at a vertex

theorem linear_equiv_is_equivalence {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) : Equivalence (linear_equiv G)

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

def firing_script (V : Type) : Type

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 V = (V → ℤ)

instance instAddCommGroupFiring_script {V : Type} : AddCommGroup (firing_script V)

Equations

• instAddCommGroupFiring_script = Pi.addCommGroup

def prin {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) : firing_script V →+ CFDiv V

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 V) (v : V) => ∑ u : V, (σ u - σ v) * ↑(num_edges G v u), map_zero' := ⋯, map_add' := ⋯ }

theorem principal_iff_eq_prin {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) : D ∈ principal_divisors G ↔ ∃ (σ : firing_script V), 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 V.

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.

instance instPartialOrderCFDiv {V : Type} : PartialOrder (CFDiv V)

Divisors form a poset, where D₁ ≤ D₂ means that for all vertices v, D₁(v) ≤ D₂(v).

Equations

• instPartialOrderCFDiv = Pi.partialOrder

def effective {V : Type} (D : CFDiv V) : 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 : V), D v ≥ 0

def Eff (V : Type) [DecidableEq V] [Fintype V] [Nonempty V] : AddSubmonoid (CFDiv V)

The submonoid of Effective divisors is denoted Eff V.

Equations

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

@[simp]

theorem mem_Eff {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {D : CFDiv V} : D ∈ Eff V ↔ effective D

def eff_one_chip {V : Type} [DecidableEq V] (v : V) : effective (one_chip v)

A one-chip divisor is effective.

Equations

• ⋯ = ⋯

theorem eff_iff_geq_zero {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (D : CFDiv V) : effective D ↔ D ≥ 0

D is effective iff D ≥ 0.

theorem sub_eff_iff_geq {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (D₁ D₂ : CFDiv V) : effective (D₁ - D₂) ↔ D₁ ≥ D₂

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

def winnable {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) : 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 V, 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 {V : Type} [Fintype V] : CFDiv V →+ ℤ

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

Equations

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

@[simp]

theorem deg_one_chip {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (v : V) : deg (one_chip v) = 1

theorem deg_of_eff_nonneg {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (D : CFDiv V) : effective D → deg D ≥ 0

Effective divisors have nonnegative degree.

theorem eff_degree_zero {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (D : CFDiv V) : effective D → deg D = 0 → D = 0

The only effective divisor of degree 0 is 0.

theorem deg_firing_vector_eq_zero {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (v_fire : V) : deg (firing_vector G v_fire) = 0

The degree of a firing vector is zero.

theorem degree_of_principal_divisor_is_zero {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (h : CFDiv V) : h ∈ principal_divisors G → deg h = 0

Every principal divisor has degree zero.

theorem linear_equiv_preserves_deg {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D D' : CFDiv V) (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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (E'' : CFDiv V) (k₁ k₂ : ℕ) (h_effective : effective E'') (h_deg : deg E'' = ↑k₁ + ↑k₂) : ∃ (E₁ : CFDiv V) (E₂ : CFDiv V), 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 {V : Type} [DecidableEq V] [Nonempty V] [Fintype V] (G : CFGraph V) : Matrix V 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 {V : Type} [DecidableEq V] [Nonempty V] [Fintype V] (G : CFGraph V) (σ : firing_script V) (D : CFDiv V) : CFDiv V

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 {V : Type} (q : V) (D : CFDiv V) : 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 : V), v ≠ q → D v ≥ 0

structure q_eff_div (V : Type) [DecidableEq V] [Fintype V] [Nonempty V] (q : V) : Type

A divisor that is q-effective.

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

def benevolent {V : Type} [DecidableEq V] [Nonempty V] [Fintype V] (G : CFGraph V) (S : Finset 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 V), ∃ (E : CFDiv V), linear_equiv G D E ∧ ∀ (v : V), E v < 0 → v ∈ S

@[irreducible]

theorem benevolent_of_nonempty {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] {G : CFGraph V} (h_conn : graph_connected G) (S : Finset V) (h_nonempty : S.Nonempty) : benevolent G S

In a connected graph, any nonempty set is benevolent.

theorem q_effective_exists {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] {G : CFGraph V} (h_conn : graph_connected G) (q : V) (D : CFDiv V) : ∃ (E : CFDiv V), 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 {V : Type} [DecidableEq V] [Nonempty V] [Fintype V] (G : CFGraph V) (q : V) (σ : firing_script V) : 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 : V), σ q ≤ σ v

def reduces_to {V : Type} [DecidableEq V] [Nonempty V] [Fintype V] (G : CFGraph V) (q : V) (D₁ D₂ : CFDiv V) : 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 V), q_reducer G q σ ∧ D₂ = D₁ + (prin G) σ

theorem reduces_to_reflexive {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] (G : CFGraph V) (q : V) (D : CFDiv V) : reduces_to G q D D

The reduces_to relation is reflexive: any divisor reduces to itself via the zero script.

theorem reduces_to_transitive {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] (G : CFGraph V) (q : V) (D₁ D₂ D₃ : CFDiv V) : reduces_to G q D₁ D₂ → reduces_to G q D₂ D₃ → reduces_to G q D₁ D₃

The reduces_to relation is transitive: composing two $q$-reducer scripts yields a $q$-reducer script.

theorem constant_script_of_zero_prin {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] {G : CFGraph V} (h_conn : graph_connected G) (σ : firing_script V) : (prin G) σ = 0 → ∀ (v w : V), σ v = σ w

In a connected graph, a firing script with zero principal divisor must be constant. This is the key step in proving antisymmetry of reduces_to.

theorem reduces_to_antisymmetric {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] {G : CFGraph V} (h_conn : graph_connected G) (q : V) (D₁ D₂ : CFDiv V) : reduces_to G q D₁ D₂ → reduces_to G q D₂ D₁ → D₁ = D₂

In a connected graph, the reduces_to relation is antisymmetric, completing the proof that it is a partial order on $q$-effective divisors.

q-reduced divisors

A $q$-effective divisor $D$ is $q$-reduced if, for every nonempty set $S \subseteq 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 {V : Type} [DecidableEq V] [Nonempty V] [Fintype V] (G : CFGraph V) (q : V) (D : CFDiv V) : 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 : V | x ≠ q}, S.Nonempty → ∃ v ∈ S, D v < ∑ w : V with w ∉ S, ↑(num_edges G v w))

theorem maxset_of_script {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] (G : CFGraph V) (σ : firing_script V) : ∃ (S : Finset V), Nonempty ↥S ∧ ∀ v ∈ S, (∀ (w : V), σ w ≤ σ v ∧ (w ∈ S → σ w = σ v)) ∧ -(prin G) σ v ≥ ∑ w : V with w ∉ S, ↑(num_edges G v w)

Helper lemma: a firing script can be understood as first firing the set where the maximum occurs, and no debt is created at this step unless it will remain at the end.

theorem q_reducer_of_add_princ_reduced {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] (G : CFGraph V) (q : V) (D : CFDiv V) (σ : firing_script V) : q_reduced G q (D + (prin G) σ) → q_effective q D → q_reducer G q σ

Helper lemma: a q-reduced divisor is only equivalent to a q-effective divisor via a q-reducer, i.e. a script that doesn't fire at q.

theorem maximum_of_q_reduced {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] (G : CFGraph V) {q : V} {D : CFDiv V} (q_eff : q_effective q D) : q_reduced G q D → ∀ (D' : CFDiv V), linear_equiv G D D' → q_effective q D' → reduces_to G q D' D

Alternative description of q-reduced divisors: maximum q-effective diviors with respect to reduction in a linear equivalence class..

theorem q_reduced_of_maximal {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] {G : CFGraph V} (h_conn : graph_connected G) {q : V} {D : CFDiv V} (q_eff : q_effective q D) : (∀ (D' : CFDiv V), linear_equiv G D D' → q_effective q D' → reduces_to G q D' D) → q_reduced G q D

For connected graphs, the converse is true: if a divisor is q_reduced, then it is maximal in the q-reduction partial order.

theorem helper_q_reduced_of_effective_is_effective {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] (G : CFGraph V) (q : V) (E E' : CFDiv V) : effective E → linear_equiv G E E' → q_reduced G q E' → effective E'

Lemma: The q-reduced representative of an effective divisor is effective. This follows from the fact that the reduction process (like Dhar's algorithm or repeated legal firings) preserves effectiveness when starting with an effective divisor.

theorem effective_of_winnable_and_q_reduced {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] (G : CFGraph V) (q : V) (D : CFDiv V) : winnable G D → q_reduced G q D → effective D

A winnable $q$-reduced divisor is effective.

theorem q_reduced_unique {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] (G : CFGraph V) (q : V) (D₁ D₂ : CFDiv V) : 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 {V : Type} [DecidableEq V] [Nonempty V] [Fintype V] (G : CFGraph V) (q : V) (D : CFDiv V) (v : 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 V), q_reducer G q σ ∧ q_effective q (D + (prin G) σ) ∧ σ q < σ v

theorem q_reduced_of_no_active {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] (G : CFGraph V) {q : V} {D : CFDiv V} (h_eff : q_effective q D) (h_no_active : ∀ (v : V), ¬active G q D v) : q_reduced G q D

A $q$-effective divisor with no active vertices is $q$-reduced.

noncomputable def reduction_excess {V : Type} [DecidableEq V] [Nonempty V] [Fintype V] (G : CFGraph V) (q : V) (D : CFDiv V) : ℤ

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 : V, if active G q D v then D v else 0

theorem reduction_excess_nonneg {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] (G : CFGraph V) {q : V} {D : CFDiv V} (h_eff : q_effective q D) : 0 ≤ reduction_excess G q D

The reduction excess is nonnegative for $q$-effective divisors, since active vertices satisfy v ≠ q and thus D v ≥ 0.

@[irreducible]

theorem q_effective_to_q_reduced {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] {G : CFGraph V} (h_conn : graph_connected G) {q : V} {D : CFDiv V} (h_eff : q_effective q D) : ∃ (E : CFDiv V), 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] {G : CFGraph V} (h_conn : graph_connected G) (q : V) (D : CFDiv V) : ∃ (D' : CFDiv V), 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] {G : CFGraph V} (h_conn : graph_connected G) (q : V) (D : CFDiv V) : ∃! D' : CFDiv V, 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] [Fintype V] {G : CFGraph V} (h_conn : graph_connected G) (q : V) (D : CFDiv V) : winnable G D ↔ ∃ (D' : CFDiv V), 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.