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 ChipFiring.CF.isEffective {G : CFGraph} (D : CFDiv G) : Bool

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

Equations

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

def ChipFiring.CF.divisorMagnitude (G : CFGraph) (D : CFDiv G) : ℕ

A small size measure used only to set conservative default loop fuel.

Equations

• ChipFiring.CF.divisorMagnitude G D = ∑ v : G.V, (D v).natAbs

def ChipFiring.CF.greedyFuel (G : CFGraph) (D : CFDiv G) : ℕ

Default fuel for greedy routines, scaled by the actual chip counts in the input.

Equations

• ChipFiring.CF.greedyFuel G D = (Fintype.card G.V + 1) * (ChipFiring.CF.divisorMagnitude G D + 1) ^ 2 + 1

def ChipFiring.CF.nonSourceChipCount (G : CFGraph) (q : G.V) (D : CFDiv G) : ℕ

Number of chips away from the source, used for the q-reduction loop budget.

Equations

• ChipFiring.CF.nonSourceChipCount G q D = ∑ v ∈ Finset.univ.erase q, (D v).toNat

@[irreducible]

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

Fuel-bounded greedy borrowing loop, recording vertices visited and the accumulated firing script.

Equations

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

noncomputable def ChipFiring.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

• ChipFiring.CF.greedyWinnable G D = ChipFiring.CF.greedyWinnableLoop G D ∅ 0 (ChipFiring.CF.greedyFuel G D)

noncomputable def ChipFiring.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.

@[irreducible]

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

Fuel-bounded deletion of burnable vertices, returning the remaining stable set.

Equations

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

noncomputable def ChipFiring.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

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

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

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

Equations

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

@[irreducible]

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

Fuel-bounded borrowing loop that seeks nonnegative wealth away from the distinguished vertex.

Equations

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

noncomputable def ChipFiring.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

• ChipFiring.CF.makeNonNegativeExceptQ G q D max_fuel = ChipFiring.CF.makeNonNegativeExceptQLoop G q D max_fuel

@[irreducible]

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

Fuel-bounded reduction loop that fires the nonburning set. Returns none if the fuel runs out before reduction completes.

Equations

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

noncomputable def ChipFiring.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 or reduction exhausts its fuel.

Equations

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

noncomputable def ChipFiring.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

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

noncomputable def ChipFiring.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

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

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

Attempts to determine winnability with a fuel-bounded reduction.

An already effective divisor returns some true, including on disconnected graphs. Otherwise this seeks the $q$-reduced representative $D_q$ and returns some (D_q(q) ≥ 0) (see Corry-Perkinson, preliminary version, Corollary 3.8). If reduction exhausts its fuel, none records an inconclusive search, not unwinnability.

Equations

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

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

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

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

Equations

• ChipFiring.CF.burningIndeg G B v = ∑ u ∈ B, ↑(ChipFiring.numEdges G u v)

@[irreducible]

noncomputable def ChipFiring.CF.dharBurningSetWithOrientationLoop (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)

Fuel-bounded burning loop that records the orientations created as vertices burn.

Equations

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

noncomputable def ChipFiring.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

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