Orientations of chip-firing graphs

This file defines orientations of chip-firing graphs and establishes their relationship to divisors, configurations, and the Riemann-Roch theorem.

An orientation (CFOrientation G) assigns a direction to each edge of G. The key objects are:

• indeg G O v: in-degree of vertex v under orientation $\mathcal{O}$.
• ordiv G O: the divisor $D(\mathcal{O})$ assigning $\mathrm{indeg}(v) - 1$ to each vertex.
• orientation_to_config G O q: the configuration $c(\mathcal{O})$ for acyclic orientations with unique source q.

The main results are:

• Theorem 4.8 ([Corry-Perkinson]): There is a bijection between acyclic orientations with unique source q and maximal superstable configurations (orientation_superstable_bijection).
• The divisor of an acyclic orientation is unwinnable (ordiv_unwinnable).
• The canonical divisor $K_G = D(\mathcal{O}) + D(\overline{\mathcal{O}})$ where $\overline{\mathcal{O}}$ is the reverse orientation (divisor_reverse_orientation).
• The handshaking theorem: $\sum_v \deg(v) = 2|E|$ (helper_sum_vertex_degrees).

structure CFOrientation (G : CFGraph) : Type u_1

An orientation of G assigns a direction to each edge: directed_edges is a multiset of directed pairs summing to G.edges (with each undirected edge directed exactly one way). The count_preserving field ensures total flow on each edge equals its multiplicity, and no_bidirectional ensures no edge is directed both ways.

• directed_edges : Multiset (G.V × G.V)

  The set of directed edges in the orientation

• count_preserving (v w : G.V) : num_edges G v w = Multiset.count (v, w) self.directed_edges + Multiset.count (w, v) self.directed_edges

  Preserves edge counts between vertex pairs

• no_bidirectional (v w : G.V) : Multiset.count (v, w) self.directed_edges = 0 ∨ Multiset.count (w, v) self.directed_edges = 0

  No bidirectional edges in the orientation

@[reducible, inline]

abbrev flow {G : CFGraph} (O : CFOrientation G) (u v : G.V) : ℕ

The flow from u to v under orientation O: the multiplicity of the directed edge (u,v).

Equations

• flow O u v = Multiset.count (u, v) O.directed_edges

def indeg (G : CFGraph) (O : CFOrientation G) (v : G.V) : ℕ

Number of edges directed into a vertex under an orientation

Equations

• indeg G O v = (Multiset.filter (fun (e : G.V × G.V) => e.2 = v) O.directed_edges).card

def outdeg (G : CFGraph) (O : CFOrientation G) (v : G.V) : ℕ

Number of edges directed out of a vertex under an orientation

Equations

• outdeg G O v = (Multiset.filter (fun (e : G.V × G.V) => e.1 = v) O.directed_edges).card

def is_source (G : CFGraph) (O : CFOrientation G) (v : G.V) : Prop

A vertex is a source if it has no incoming edges (indegree = 0)

Equations

• is_source G O v = (indeg G O v = 0)

def is_sink (G : CFGraph) (O : CFOrientation G) (v : G.V) : Prop

A vertex is a sink if it has no outgoing edges (outdegree = 0)

Equations

• is_sink G O v = (outdeg G O v = 0)

def directed_edge (G : CFGraph) (O : CFOrientation G) (u v : G.V) : Prop

directed_edge G O u v holds when there is a directed edge from u to v in orientation O.

Equations

• directed_edge G O u v = ((u, v) ∈ O.directed_edges)

def list_get_safe {α : Type} (l : List α) (i : ℕ) : Option α

Helper function for safe list access

Equations

• list_get_safe l i = if h : i < l.length then some (l.get ⟨i, h⟩) else none

structure DirectedPath {G : CFGraph} (O : CFOrientation G) : Type u_1

A directed path in a graph under an orientation

• vertices : List G.V

  The sequence of vertices in the path

• non_empty : self.vertices.length > 0

  Path must not be empty (at least one vertex)

• valid_edges : List.IsChain (directed_edge G O) self.vertices

  Every consecutive pair forms a directed edge

def non_repeating {G : CFGraph} {O : CFOrientation G} (p : DirectedPath O) : Prop

A directed path is non-repeating if its vertex list has no duplicates.

Equations

• non_repeating p = p.vertices.Nodup

def is_acyclic (G : CFGraph) (O : CFOrientation G) : Prop

An orientation is acyclic if it has no directed cycles and maintains consistent edge directions between vertices

Equations

• is_acyclic G O = ∀ (p : DirectedPath O), non_repeating p

noncomputable def ancestors (G : CFGraph) (O : CFOrientation G) (v : G.V) : Finset G.V

The set of ancestors of a vertex v (nodes x such that there is a path x -> ... -> v)

Equations

• ancestors G O v = {x : G.V | Relation.TransGen (fun (a b : G.V) => directed_edge G O a b) x v}

noncomputable def vertexLevelMeasure (G : CFGraph) (O : CFOrientation G) (v : G.V) : ℕ

Measure for vertex_level termination: number of ancestors.

Equations

• vertexLevelMeasure G O v = (ancestors G O v).card

def acyclic_with_unique_source (G : CFGraph) (O : CFOrientation G) (q : G.V) : Prop

acyclic_with_unique_source G O q means that O is acyclic and every source of O is equal to q.

Equations

• acyclic_with_unique_source G O q = (is_acyclic G O ∧ ∀ (w : G.V), is_source G O w → w = q)

def config_of_source {G : CFGraph} {O : CFOrientation G} {q : G.V} (hO : acyclic_with_unique_source G O q) : Config G q

The configuration associated to an acyclic orientation with unique source q: assigns $\mathrm{indeg}(v) - 1$ chips to each vertex $v \neq q$, and $0$ at $q$.

Equations

• config_of_source hO = { vertex_degree := fun (v : G.V) => if v = q then 0 else ↑(indeg G O v) - 1, q_zero := ⋯, non_negative := ⋯ }

Orientation divisors and configurations

For an orientation $\mathcal{O}$ of $G$, the orientation divisor ordiv G O is $D(\mathcal{O})(v) = \mathrm{indeg}_{\mathcal{O}}(v) - 1$ ([Corry-Perkinson], Definition 4.7).

For an acyclic orientation $\mathcal{O}$ with unique source $q$, the associated configuration orientation_to_config G O q assigns $\mathrm{indeg}(v) - 1$ chips to each non-$q$ vertex. An acyclic orientation is uniquely determined by its in-degree sequence (orientation_determined_by_indegrees), and the divisor of an acyclic orientation is always $q$-reduced and unwinnable.

def ordiv (G : CFGraph) (O : CFOrientation G) : CFDiv G

The divisor associated with an orientation assigns indegree - 1 to each vertex [Corry-Perkinson], Definition 4.7, part 1; written D(O) there.

Equations

• ordiv G O v = ↑(indeg G O v) - 1

def orqed {G : CFGraph} (O : CFOrientation G) {q : G.V} (hO : acyclic_with_unique_source G O q) : q_eff_div G q

The orientation divisor ordiv G O bundled as a q_eff_div, using acyclicity to prove $q$-effectivity.

Equations

• orqed O hO = { D := ordiv G O, h_eff := ⋯ }

def orientation_to_config (G : CFGraph) (O : CFOrientation G) (q : G.V) (hO : acyclic_with_unique_source G O q) : Config G q

The configuration c(O) associated to an acyclic orientation O. [Corry-Perkinson], Definition 4.7 (part 2)

Equations

• orientation_to_config G O q hO = config_of_source hO

theorem config_and_divisor_from_O {G : CFGraph} (O : CFOrientation G) {q : G.V} (hO : acyclic_with_unique_source G O q) : orientation_to_config G O q hO = toConfig (orqed O hO)

Compatibility between configurations and divisors from an orientation

theorem orientation_determined_by_indegrees {G : CFGraph} (O O' : CFOrientation G) : is_acyclic G O → is_acyclic G O' → (∀ (v : G.V), indeg G O v = indeg G O' v) → O = O'

An acyclic orientation is uniquely determined by its indegree sequence. See [Corry-Perkinson], Lemma 4.3.

theorem degree_ordiv {G : CFGraph} (O : CFOrientation G) : deg (ordiv G O) = genus G - 1

The degree of an orientation divisor equals $g - 1$, where $g$ is the genus of $G$.

theorem config_degree_from_O {G : CFGraph} (O : CFOrientation G) {q : G.V} (hO : acyclic_with_unique_source G O q) : config_degree (orientation_to_config G O q hO) = genus G

The configuration degree of an acyclic orientation with unique source equals the genus.

theorem ordiv_unwinnable (G : CFGraph) (O : CFOrientation G) : is_acyclic G O → ¬winnable G (ordiv G O)

The orientation divisor $D(\mathcal{O})$ of an acyclic orientation $\mathcal{O}$ is not winnable. This is part of [Corry-Perkinson], Proposition 4.11.

The canonical divisor and reverse orientations

The canonical divisor of $G$ is $K_G(v) = \deg(v) - 2$ for each vertex $v$ ([Corry-Perkinson], Definition 4.7). The reverse orientation $\overline{\mathcal{O}}$ of an orientation $\mathcal{O}$ is obtained by reversing all edge directions. The key identity is $D(\mathcal{O}) + D(\overline{\mathcal{O}}) = K_G$ (divisor_reverse_orientation).

This section also contains the handshaking theorem (helper_sum_vertex_degrees): $\sum_{v \in G.V} \deg(v) = 2|E|$, and its corollary that $\deg(K_G) = 2g - 2$ (degree_of_canonical_divisor).

def canonical_divisor (G : CFGraph) : CFDiv G

The canonical divisor assigns degree - 2 to each vertex. This is independent of orientation and equals D(O) + D(reverse(O))

Equations

• canonical_divisor G v = vertex_degree G v - 2

def CFOrientation.reverse (G : CFGraph) (O : CFOrientation G) : CFOrientation G

The reverse orientation $\overline{\mathcal{O}}$ obtained by reversing all edge directions. See [Corry-Perkinson], Definition 5.7.

Equations

• CFOrientation.reverse G O = { directed_edges := Multiset.map Prod.swap O.directed_edges, count_preserving := ⋯, no_bidirectional := ⋯ }

theorem is_acyclic_reverse_of_is_acyclic (G : CFGraph) (O : CFOrientation G) (h_acyclic : is_acyclic G O) : is_acyclic G (CFOrientation.reverse G O)

The reverse of an acyclic orientation is also acyclic.

theorem divisor_reverse_orientation {G : CFGraph} (O : CFOrientation G) : ordiv G O + ordiv G (CFOrientation.reverse G O) = canonical_divisor G

The orientation divisors of $\mathcal{O}$ and its reverse sum to the canonical divisor: $D(\mathcal{O}) + D(\overline{\mathcal{O}}) = K_G$.

theorem degree_of_canonical_divisor (G : CFGraph) : deg (canonical_divisor G) = 2 * genus G - 2

The degree of the canonical divisor is $2g - 2$, where $g$ is the genus of $G$. This is [Corry-Perkinson], Exercise 5.8.

Orientations from burn lists

Given a complete burn list L for a superstable configuration c, the function burn_orientation L h_full constructs an acyclic orientation of G with unique source q (burn_acyclic, burn_unique_source). Acyclicity is proved by showing that position in the burn list gives a strictly decreasing labeling along any directed path (dp_dec).

The key lemma dp_dec formalizes this as a strict chain of natural numbers, and orientation_from_flow constructs a CFOrientation from an explicit flow function.

def multiset_of_count {T : Type u_1} [DecidableEq T] [Fintype T] (f : T → ℕ) : Multiset T

Create a multiset with a given count function. This is a thin wrapper around DFinsupp.toMultiset specialized to a finite type.

Equations

• multiset_of_count f = DFinsupp.toMultiset (DFinsupp.equivFunOnFintype.symm f)

def orientation_from_flow {G : CFGraph} (f : G.V × G.V → ℕ) (h_count_preserving : ∀ (v w : G.V), f (v, w) + f (w, v) = num_edges G v w) (h_no_bidirectional : ∀ (v w : G.V), f (v, w) = 0 ∨ f (w, v) = 0) : CFOrientation G

Construct a CFOrientation from an explicit flow function, given proofs that it respects edge multiplicities and has no bidirectional edges.

Equations

• orientation_from_flow f h_count_preserving h_no_bidirectional = { directed_edges := multiset_of_count f, count_preserving := ⋯, no_bidirectional := ⋯ }

def burn_orientation {G : CFGraph} {q : G.V} {c : Config G q} (L : burn_list G c) (h_full : ∀ (v : G.V), v ∈ L.list) : CFOrientation G

The orientation constructed from a complete burn list L for a superstable configuration, via burn_flow. This is shown to be acyclic with unique source $q$ by burn_acyclic and burn_unique_source.

Equations

• burn_orientation L h_full = orientation_from_flow (burn_flow L) ⋯ ⋯

The bijection between orientations and maximal superstable configurations

This section establishes [Corry-Perkinson], Theorem 4.8: there is a bijection between acyclic orientations with unique source $q$ and maximal superstable configurations.

• superstable_dhar: Given a superstable configuration c, Dhar's algorithm produces an acyclic orientation whose associated configuration dominates c.
• orientation_config_maximal: Every acyclic orientation with unique source $q$ gives a maximal superstable configuration.
• maximal_superstable_orientation: Every maximal superstable configuration arises from some acyclic orientation.
• orientation_superstable_bijection: The full bijection statement.

theorem superstable_dhar {G : CFGraph} {q : G.V} {c : Config G q} (h_ss : superstable G q c) : ∃ (O : CFOrientation G) (hO : acyclic_with_unique_source G O q), c ≤ orientation_to_config G O q hO

Theorem: Dhar's burning algorithm produces, from a superstable configuration, an orientation giving a maximal superstable above it.

theorem orientation_config_maximal (G : CFGraph) (O : CFOrientation G) (q : G.V) (hO : acyclic_with_unique_source G O q) : maximal_superstable G (orientation_to_config G O q hO)

The configuration asssociated to an acyclic orientation with unique source is maximal superstable. [Corry-Perkinson], Theorem 4.8, part 1 (c(O) is maximal superstable)

theorem maximal_superstable_exists (G : CFGraph) (q : G.V) (c : Config G q) (h_super : superstable G q c) : ∃ (c' : Config G q), maximal_superstable G c' ∧ c ≤ c'

Every superstable configuration extends to a maximal superstable configuration

theorem maximal_superstable_orientation (G : CFGraph) (q : G.V) (c : Config G q) (h_max : maximal_superstable G c) : ∃ (O : CFOrientation G) (hO : acyclic_with_unique_source G O q), orientation_to_config G O q hO = c

Every maximal superstable configuration comes from an acyclic orientation [Corry-Perkinson], Theorem 4.8, part 2 (surjectivity)

theorem orientation_superstable_bijection (G : CFGraph) (q : G.V) : let α := { O : CFOrientation G // acyclic_with_unique_source G O q }; let β := { c : Config G q // maximal_superstable G c }; let f_raw := fun (O_sub : α) => orientation_to_config G (↑O_sub) q ⋯; have f := fun (O_sub : α) => ⟨f_raw O_sub, ⋯⟩; Function.Bijective f

Bijection between acyclic orientations with source q and maximal superstable configurations Corry-Perkinson], Theorem 4.8, part 3 (bijection)