Basic

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; numEdges 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 graphConnected. 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

  The finite nonempty type of graph vertices.

• instDecidableEq : DecidableEq self.V
• instFintype : Fintype self.V
• instNonempty : Nonempty self.V
• edges : Multiset (self.V × self.V)

  The multiset of endpoint pairs encoding edges, including their multiplicities.

• loopless (v : self.V) : (v, v) ∉ self.edges

def numEdges (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

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

def graphConnected (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

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

def CFGraph.genus (G : CFGraph) : ℤ

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

Equations

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

theorem num_edges_symmetric (G : CFGraph) (v w : G.V) : numEdges G v w = numEdges 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) : numEdges G v v = 0

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

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

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

Equations

• vertexDegree G v = ∑ u : G.V, ↑(numEdges 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 firingVector 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 oneChip {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

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

@[simp]

theorem one_chip_apply_v {G : CFGraph} (v : G.V) : oneChip v v = 1

@[simp]

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

@[simp]

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

def firingMove (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

• firingMove G D v w = if w = v then D v - vertexDegree G v else D w + ↑(numEdges G v w)

def borrowingMove (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

• borrowingMove G D v w = if w = v then D v + vertexDegree G v else D w - ↑(numEdges G v w)

def outdegreeSet (G : CFGraph) (S : Finset G.V) (v : G.V) : ℤ

The out-degree of v relative to S, counted with edge multiplicity.

Equations

• outdegreeSet G S v = ∑ w ∈ Finset.univ \ S, ↑(numEdges G v w)

@[simp]

theorem outdeg_S_eq_sum_filter (G : CFGraph) (S : Finset G.V) (v : G.V) : outdegreeSet G S v = ∑ w : G.V with w ∉ S, ↑(numEdges G v w)

theorem outdeg_S_nonneg (G : CFGraph) (S : Finset G.V) (v : G.V) : 0 ≤ outdegreeSet G S v

theorem outdeg_S_antitone (G : CFGraph) {S T : Finset G.V} (h : S ⊆ T) (v : G.V) : outdegreeSet G T v ≤ outdegreeSet G S v

def setFiring (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

• setFiring G D S w = if w ∈ S then D w - outdegreeSet G S w else D w + outdegreeSet G Sᶜ w

theorem set_firing_apply_of_mem (G : CFGraph) (D : CFDiv G) {S : Finset G.V} {v : G.V} (hv : v ∈ S) : setFiring G D S v = D v - outdegreeSet G S v

theorem set_firing_apply_of_not_mem (G : CFGraph) (D : CFDiv G) {S : Finset G.V} {v : G.V} (hv : v ∉ S) : setFiring G D S v = D v + outdegreeSet G Sᶜ v

theorem le_set_firing_apply_of_not_mem (G : CFGraph) (D : CFDiv G) {S : Finset G.V} {v : G.V} (hv : v ∉ S) : D v ≤ setFiring G D S v

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

The principal divisor associated to firing a single vertex.

Equations

• firingVector G v w = if w = v then -vertexDegree G v else ↑(numEdges G v w)

Principal divisors and linear equivalence

A firing script (firingScript 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 principalDivisors G is generated by the firing vectors firingVector G v for all $v$. Two divisors $D$ and $D'$ are linearly equivalent (linearEquiv 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 principalDivisors (G : CFGraph) : AddSubgroup (CFDiv G)

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

Equations

• principalDivisors G = AddSubgroup.closure (Set.range (firingVector G))

def linearEquiv (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

• linearEquiv G D D' = (D' - D ∈ principalDivisors G)

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

Linear equivalence is reflexive.

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

Linear equivalence is symmetric.

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

Linear equivalence is transitive.

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

Linear equivalence is an equivalence relation on $\operatorname{Div}(G)$.

@[reducible, inline]

abbrev firingScript (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

• firingScript G = (G.V → ℤ)

def indicatorScript (G : CFGraph) (S : Finset G.V) : firingScript G

The firing script that fires exactly the vertices in S, once each.

Equations

• indicatorScript G S v = if v ∈ S then 1 else 0

def prin (G : CFGraph) : firingScript 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 (σ : firingScript G) (v : G.V) => ∑ u : G.V, (σ u - σ v) * ↑(numEdges G v u), map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem prin_apply (G : CFGraph) (σ : firingScript G) (v : G.V) : (prin G) σ v = ∑ u : G.V, (σ u - σ v) * ↑(numEdges G v u)

@[simp]

theorem prin_const (G : CFGraph) (c : ℤ) : ((prin G) fun (x : G.V) => c) = 0

Constant firing scripts have zero principal divisor.

@[simp]

theorem prin_sub_const (G : CFGraph) (σ : firingScript G) (c : ℤ) : ((prin G) fun (v : G.V) => σ v - c) = (prin G) σ

theorem set_firing_eq_add_prin_indicator_script (G : CFGraph) (D : CFDiv G) (S : Finset G.V) : setFiring G D S = D + (prin G) (indicatorScript G S)

Firing a set once is the same as adding the principal divisor of its indicator script.

theorem principal_iff_eq_prin (G : CFGraph) (D : CFDiv G) : D ∈ principalDivisors G ↔ ∃ (σ : firingScript 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 principalDivisors 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' := ⋯ }

@[simp]

theorem mem_Eff {G : CFGraph} {D : CFDiv G} : D ∈ Eff G ↔ effective D

theorem eff_one_chip {G : CFGraph} (v : G.V) : effective (oneChip 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, linearEquiv 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 laplacianMatrix 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 CFDiv.degree {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

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

@[simp]

theorem deg_one_chip {G : CFGraph} (v : G.V) : CFDiv.degree (oneChip v) = 1

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

Effective divisors have nonnegative degree.

theorem eff_degree_zero {G : CFGraph} (D : CFDiv G) : effective D → CFDiv.degree 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 : linearEquiv G D D') : CFDiv.degree D = CFDiv.degree 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 : CFDiv.degree E'' = ↑k₁ + ↑k₂) : ∃ (E₁ : CFDiv G) (E₂ : CFDiv G), effective E₁ ∧ effective E₂ ∧ CFDiv.degree E₁ = ↑k₁ ∧ CFDiv.degree 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 laplacianMatrix (G : CFGraph) : Matrix G.V G.V ℤ

The Laplacian matrix of a CFGraph.

See: Corry-Perkinson, Definition 2.6.

Equations

• laplacianMatrix G i j = if i = j then vertexDegree G i else -↑(numEdges G i j)

def applyLaplacian (G : CFGraph) (σ : firingScript G) (D : CFDiv G) : CFDiv G

Applies the Laplacian matrix to a firing script and a current divisor to obtain a new divisor.

Equations

• applyLaplacian G σ D v = D v - (laplacianMatrix 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 qEffectiveDivisor 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 qEffective {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

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

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

A divisor bundled with a proof that it is $q$-effective.

• D : CFDiv G

  The underlying divisor, effective away from the distinguished vertex.

• h_eff : qEffective 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), linearEquiv G D E ∧ ∀ (v : G.V), E v < 0 → v ∈ S

theorem benevolent_of_nonempty {G : CFGraph} (h_conn : graphConnected 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 : graphConnected G) (q : G.V) (D : CFDiv G) : ∃ (E : CFDiv G), qEffective q E ∧ linearEquiv 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 reducesTo 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 qReducer (G : CFGraph) (q : G.V) (σ : firingScript 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

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

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

The relation reducesTo 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

• reducesTo G q D₁ D₂ = ∃ (σ : firingScript G), qReducer 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 reductionExcess — the total chips at active vertices — strictly decreases at each reduction step.

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

A set of vertices is legal for D if firing it leaves every vertex in the set nonnegative.

Equations

• legalSet G D S = ∀ v ∈ S, outdegreeSet G S v ≤ D v

@[instance_reducible]

instance instDecidableLegalSet (G : CFGraph) (D : CFDiv G) (S : Finset G.V) : Decidable (legalSet G D S)

Equations

• instDecidableLegalSet G D S = id inferInstance

@[simp]

theorem legal_set_empty (G : CFGraph) (D : CFDiv G) : legalSet G D ∅

theorem effective_set_firing_of_legal_set (G : CFGraph) {D : CFDiv G} {S : Finset G.V} (hD : effective D) (hS : legalSet G D S) : effective (setFiring G D S)

theorem q_effective_set_firing_of_legal_set (G : CFGraph) {q : G.V} {D : CFDiv G} {S : Finset G.V} (hD : qEffective q D) (hS : legalSet G D S) : qEffective q (setFiring G D S)

Firing a legal set preserves effectivity away from a distinguished vertex.

theorem legal_set_union (G : CFGraph) {D : CFDiv G} {S T : Finset G.V} (hS : legalSet G D S) (hT : legalSet G D T) : legalSet G D (S ∪ T)

def qReduced (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

• qReduced G q D = (qEffective q D ∧ ∀ (S : Finset G.V), q ∉ S → S.Nonempty → ¬legalSet G D S)

theorem qReduced.exists_lt_outdeg {G : CFGraph} {q : G.V} {D : CFDiv G} (hred : qReduced G q D) {S : Finset G.V} (hq : q ∉ S) (hS : S.Nonempty) : ∃ v ∈ S, D v < outdegreeSet G S v

A nonempty set avoiding q contains a vertex that would go into debt when fired from a q-reduced divisor.

theorem effective_of_winnable_and_q_reduced (G : CFGraph) (q : G.V) (D : CFDiv G) : winnable G D → qReduced 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) : qReduced G q D₁ ∧ qReduced G q D₂ ∧ linearEquiv 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 = ∃ (σ : firingScript G), qReducer G q σ ∧ qEffective q (D + (prin G) σ) ∧ σ q < σ v

noncomputable def reductionExcess (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

• reductionExcess 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 : graphConnected G) {q : G.V} {D : CFDiv G} (h_eff : qEffective q D) : ∃ (E : CFDiv G), qReduced G q E ∧ linearEquiv 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 reductionExcess.

theorem exists_q_reduced_representative {G : CFGraph} (h_conn : graphConnected G) (q : G.V) (D : CFDiv G) : ∃ (D' : CFDiv G), linearEquiv G D D' ∧ qReduced 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 : graphConnected G) (q : G.V) (D : CFDiv G) : ∃! D' : CFDiv G, linearEquiv G D D' ∧ qReduced 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 : graphConnected G) (q : G.V) (D : CFDiv G) : winnable G D ↔ ∃ (D' : CFDiv G), linearEquiv G D D' ∧ qReduced 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, vertexDegree 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)|. $$