Computational algorithms for chip-firing

This file implements the main computational algorithms for chip-firing on graphs:

• greedyWinnable: Greedy dollar game solver (Algorithm 1).
• dharBurningSet: Dhar's burning algorithm, returning the set of unburnt vertices (Algorithm 2).
• findQReducedDivisor: Finds the unique $q$-reduced divisor linearly equivalent to a given divisor (Algorithm 3).
• isWinnable: Winnability check via $q$-reduction (Algorithm 4).
• dharBurningSetWithOrientation: Dhar's burning algorithm with orientation tracking (Algorithm 5).

def CF.is_effective {V : Type} [Fintype V] (D : CFDiv V) : Bool

Check if a divisor is effective (all vertices non-negative). From Basic.lean

Equations

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

noncomputable def CF.greedyWinnable {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) : Bool × Option (CFDiv V)

Greedy Algorithm for the dollar game (Algorithm 1). Repeatedly chooses an in-debt vertex v that hasn't borrowed yet (v ∉ M) and performs a borrowing move at v, adding v to M. 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 (Fintype.card V * Fintype.card V)

@[irreducible]

noncomputable def CF.greedyWinnable.loop {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : CFGraph V) (current_D : CFDiv V) (M : Finset V) (script : CFDiv V) (fuel : ℕ) : Bool × Option (CFDiv V)

Equations

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

def CF.dhar_outdeg {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : CFGraph V) (S : Finset V) (v : 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). outdeg G S v = |{ w | ∃ edge (v, w) in G.edges and w ∉ S }|

Equations

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

noncomputable def CF.findBurnableVertex {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : CFGraph V) (c : V → ℤ) (S : Finset V) : Option { v : V // v ∈ S }

Find a vertex v in S such that c(v) < dhar_outdeg G S v (a "burnable" vertex). Returns some v if found, none otherwise.

Equations

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

noncomputable def CF.dharBurningSet {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : CFGraph V) (q : V) (c : V → ℤ) : Finset V

The core iterative burning process of Dhar's algorithm (Algorithm 2). Given a configuration c (represented as V → ℤ for simplicity here, assuming non-negativity outside q is handled externally) and a sink q, it finds the set of unburnt vertices S ⊆ V \ {q} which forms a legal firing set. The set S is empty if and only if c restricted to V \ {q} is superstable relative to q.

Implementation uses well-founded recursion on the size of the set S.

Equations

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

@[irreducible]

noncomputable def CF.dharBurningSet.loop {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : CFGraph V) (c : V → ℤ) (S : Finset V) (fuel : ℕ) : Finset V

Equations

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

noncomputable def CF.fireSet {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (S : Finset V) : CFDiv V

Helper function to fire a set of vertices S on a divisor D.

Equations

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

def CF.degree {V : Type} [Fintype V] (D : CFDiv V) : ℤ

Calculates the degree of a divisor.

Equations

• CF.degree D = ∑ v : V, D v

noncomputable def CF.makeNonNegativeExceptQ {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : CFGraph V) (q : V) (D : CFDiv V) (max_fuel : ℕ) : Option (CFDiv V)

Preprocessing Step for Algorithm 3/4: Fires q repeatedly until D(v) ≥ 0 for all v ≠ q. Requires sufficient total degree in the graph. Uses fuel for termination guarantee. 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 {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : CFGraph V) (q : V) (current_D : CFDiv V) (fuel : ℕ) : Option (CFDiv V)

Equations

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

noncomputable def CF.findQReducedDivisor {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : CFGraph V) (q : V) (D : CFDiv V) : Option (CFDiv V)

Finds the unique q-reduced divisor linearly equivalent to D (Algorithm 3). Starts from divisor D, performs preprocessing (firing q until others non-negative), then repeatedly finds the maximal legal firing set S ⊆ V \ {q} using dharBurningSet and fires S until dharBurningSet returns an 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 {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : CFGraph V) (q : V) (current_D : CFDiv V) (fuel : ℕ) : CFDiv V

Equations

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

noncomputable def CF.burn {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : CFGraph V) (q : V) (c : V → ℤ) : Finset V

Simulates the fire spread from q in Dhar's algorithm on a configuration c. Returns the set of unburnt vertices $S \subseteq V \setminus \{q\}$. Equivalent to dharBurningSet.

Equations

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

noncomputable def CF.dhar {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (v : V) : Option (CFDiv V)

Finds the v-reduced divisor linearly equivalent to D. Wraps findQReducedDivisor. Returns none if the reduction process fails.

Equations

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

noncomputable def CF.isWinnable {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : CFGraph V) (q : V) (D : CFDiv V) : Bool

Efficient Winnability Determination Algorithm (Algorithm 4). Checks if the divisor D is winnable by finding the q-reduced equivalent Dq and checking if Dq(q) ≥ 0. Requires selection of a source vertex q. Returns false if 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 {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : CFGraph V) (B : Finset V) (v : V) : ℤ

Helper to calculate incoming "burning" degree for vertex v from set B. Sums num_edges from u in B to v.

Equations

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

noncomputable def CF.dharBurningSetWithOrientation {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : CFGraph V) (q : V) (c : V → ℤ) : Finset V × Multiset (V × V)

Orientation-based Dhar's Algorithm (Algorithm 5). Takes a nonnegative configuration c relative to q. Returns the final stable set S ⊆ V \ {q} (empty iff c is superstable) and a multiset O of directed edges (u, v) where fire spread from u to v.

Note: Assumes c is non-negative on V \ {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 V + 1)

@[irreducible]

noncomputable def CF.dharBurningSetWithOrientation.loop {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : CFGraph V) (c : V → ℤ) (current_S current_B : Finset V) (current_O : Multiset (V × V)) (fuel : ℕ) : Finset V × Multiset (V × V)

Equations

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