Experimental computational algorithms for chip-firing

This file contains an early executable implementation of several chip-firing algorithms, including greedy dollar-game play, Dhar's burning algorithm, and $q$-reduction routines.

The formal proof of Riemann-Roch in this repository does not rely on this file. Some of these definitions predate the current theorem-proving infrastructure and should be treated as exploratory code rather than certified implementations of the textbook algorithms. In particular, the core mathematical statements about $q$-reduced divisors, superstability, and Dhar's algorithm are proved elsewhere in the library.

def CF.is_effective {G : CFGraph} (D : CFDiv G) : Bool

Checks whether a divisor is effective, meaning that all vertex values are nonnegative.

Equations

• CF.is_effective D = decide (∀ (v : G.V), D v ≥ 0)

noncomputable def CF.greedyWinnable (G : CFGraph) (D : CFDiv G) : Bool × Option (CFDiv G)

The greedy algorithm for the dollar game (Corry-Perkinson, Algorithm 1).

The algorithm repeatedly chooses an in-debt vertex $v$, performs a borrowing move at $v$, and records in $M$ that $v$ has borrowed at least once. Vertices already in $M$ may still need to borrow again. Returns (winnable, script) where winnable is true if an effective divisor is reached, and script is the net borrowing count for each vertex if winnable.

Equations

• CF.greedyWinnable G D = CF.greedyWinnable.loop G D ∅ 0 (CF.greedyFuel✝ G D)

@[irreducible]

noncomputable def CF.greedyWinnable.loop (G : CFGraph) (current_D : CFDiv G) (M : Finset G.V) (script : CFDiv G) (fuel : ℕ) : Bool × Option (CFDiv G)

Equations

• One or more equations did not get rendered due to their size.

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

Calculates the out-degree of a vertex $v$ with respect to a set $S$.

This counts the number of edges from $v$ to vertices outside $S$, including $q$: $$ \operatorname{outdeg}_S(v) = |\{w \mid \text{there is an edge from } v \text{ to } w \text{ and } w \notin S\}|. $$

Equations

• CF.dhar_outdeg G S v = ∑ w : G.V with w ∉ S, ↑(num_edges G v w)

noncomputable def CF.findBurnableVertex (G : CFGraph) (c : G.V → ℤ) (S : Finset G.V) : Option ↥S

Finds a burnable vertex $v \in S$, meaning one satisfying $c(v) < \operatorname{outdeg}_S(v)$.

Returns some v if found, none otherwise.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CF.dharBurningSet (G : CFGraph) (q : G.V) (c : G.V → ℤ) : Finset G.V

The core iterative burning process of Dhar's algorithm (Corry-Perkinson, Algorithm 2).

Given a configuration $c$ (represented here as a function $V(G) \to \mathbb{Z}$, with nonnegativity away from $q$ handled externally) and a sink $q$, this returns the set of unburnt vertices $S \subseteq V(G) \setminus \{q\}$. The set $S$ is empty if and only if the restriction of $c$ to $V(G) \setminus \{q\}$ is superstable relative to $q$.

The implementation uses well-founded recursion on the size of $S$.

Equations

• CF.dharBurningSet G q c = CF.dharBurningSet.loop G c (Finset.univ.erase q) (Fintype.card G.V + 1)

@[irreducible]

noncomputable def CF.dharBurningSet.loop (G : CFGraph) (c : G.V → ℤ) (S : Finset G.V) (fuel : ℕ) : Finset G.V

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CF.fireSet (G : CFGraph) (D : CFDiv G) (S : Finset G.V) : CFDiv G

Fires every vertex in $S$, starting from the divisor $D$.

Equations

• CF.fireSet G D S = List.foldl (fun (current_D : CFDiv G) (v : G.V) => firing_move G current_D v) D S.toList

noncomputable def CF.makeNonNegativeExceptQ (G : CFGraph) (q : G.V) (D : CFDiv G) (max_fuel : ℕ) : Option (CFDiv G)

The preprocessing step for findQReducedDivisor.

This borrows greedily at in-debt non-source vertices until $D(v) \ge 0$ for all $v \ne q$ (Corry-Perkinson, Algorithm 4). Requires sufficient fuel for the termination guard. Returns none if fuel runs out, implying potential unwinnability or insufficient fuel.

Equations

• CF.makeNonNegativeExceptQ G q D max_fuel = CF.makeNonNegativeExceptQ.loop G q D max_fuel

@[irreducible]

noncomputable def CF.makeNonNegativeExceptQ.loop (G : CFGraph) (q : G.V) (current_D : CFDiv G) (fuel : ℕ) : Option (CFDiv G)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CF.findQReducedDivisor (G : CFGraph) (q : G.V) (D : CFDiv G) : Option (CFDiv G)

Finds the unique $q$-reduced divisor linearly equivalent to $D$ (Corry-Perkinson, Algorithm 3).

Starting from $D$, the algorithm first preprocesses by borrowing greedily at in-debt non-source vertices until all vertices other than $q$ are nonnegative. It then repeatedly finds the maximal legal firing set $S \subseteq V(G) \setminus \{q\}$ using dharBurningSet, and fires $S$ until dharBurningSet returns the empty set.

Returns none if preprocessing fails (fuel exhaustion or insufficient degree).

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

noncomputable def CF.findQReducedDivisor.loop (G : CFGraph) (q : G.V) (current_D : CFDiv G) (fuel : ℕ) : CFDiv G

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CF.burn (G : CFGraph) (q : G.V) (c : G.V → ℤ) : Finset G.V

Simulates the fire spread from $q$ in Dhar's algorithm on a configuration $c$.

Returns the set of unburnt vertices $S \subseteq V(G) \setminus \{q\}$. Equivalent to dharBurningSet.

Equations

• CF.burn G q c = CF.dharBurningSet G q c

noncomputable def CF.dhar (G : CFGraph) (D : CFDiv G) (v : G.V) : Option (CFDiv G)

Finds the $v$-reduced divisor linearly equivalent to $D$.

This wraps findQReducedDivisor. Returns none if the reduction process fails.

Equations

• CF.dhar G D v = CF.findQReducedDivisor G v D

noncomputable def CF.isWinnable (G : CFGraph) (q : G.V) (D : CFDiv G) : Bool

The efficient winnability determination algorithm.

This checks whether $D$ is winnable by finding the $q$-reduced representative $D_q$ and checking whether $D_q(q) \ge 0$ (see Corry-Perkinson, Corollary 3.7). It requires a chosen source vertex $q$ and returns false if the reduction process fails.

Equations

• CF.isWinnable G q D = match CF.findQReducedDivisor G q D with | none => false | some D_q => decide (D_q q ≥ 0)

def CF.burning_indeg (G : CFGraph) (B : Finset G.V) (v : G.V) : ℤ

Calculates the incoming burning degree of a vertex $v$ from a set $B$.

This sums num_edges from each $u \in B$ to $v$.

Equations

• CF.burning_indeg G B v = ∑ u ∈ B, ↑(num_edges G u v)

noncomputable def CF.dharBurningSetWithOrientation (G : CFGraph) (q : G.V) (c : G.V → ℤ) : Finset G.V × Multiset (G.V × G.V)

The orientation-based version of Dhar's algorithm (Corry-Perkinson, Algorithm 5).

This takes a nonnegative configuration $c$ relative to $q$, and returns the final stable set $S \subseteq V(G) \setminus \{q\}$ (empty if and only if $c$ is superstable) together with a multiset $O$ of directed edges $(u,v)$ where fire spread from $u$ to $v$.

Note: this assumes $c$ is nonnegative on $V(G) \setminus \{q\}$. The returned multiset O represents the edges oriented by the burning process. It may not form a complete CFOrientation structure directly if not all edges are involved.

Equations

• CF.dharBurningSetWithOrientation G q c = CF.dharBurningSetWithOrientation.loop G c (Finset.univ.erase q) {q} ∅ (Fintype.card G.V + 1)

@[irreducible]

noncomputable def CF.dharBurningSetWithOrientation.loop (G : CFGraph) (c : G.V → ℤ) (current_S current_B : Finset G.V) (current_O : Multiset (G.V × G.V)) (fuel : ℕ) : Finset G.V × Multiset (G.V × G.V)

Equations

• One or more equations did not get rendered due to their size.