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

theorem opp_flow {G : CFGraph} (O : CFOrientation G) (u v : G.V) : flow O u v + flow O v u = num_edges G u v

The total flow on an undirected edge equals its multiplicity: flow O u v + flow O v u = num_edges G u v.

theorem eq_orient {G : CFGraph} (O1 O2 : CFOrientation G) : O1 = O2 ↔ ∀ (u v : G.V), flow O1 u v = flow O2 u v

Two orientations are equal iff they assign the same flow to every directed pair.

theorem double_sum {T : Type u_1} [DecidableEq T] [Fintype T] (f : T × T → ℕ) : ∑ u : T, ∑ v : T, f (u, v) = ∑ e : T × T, f e

Helper lema for the count below.

theorem card_directed_edges_eq_card_edges {G : CFGraph} (O : CFOrientation G) : O.directed_edges.card = G.edges.card

Helper lemma for later calculations. Puzzlingly intricate for such a simple statement! Perhaps it can be simplified.

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

theorem indeg_eq_sum_flow {G : CFGraph} (O : CFOrientation G) (v : G.V) : indeg G O v = ∑ w : G.V, flow O w v

The in-degree of v equals the sum of flows into v from all vertices.

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

theorem path_length_bound {G : CFGraph} {O : CFOrientation G} (p : DirectedPath O) : non_repeating p → p.vertices.length ≤ Fintype.card G.V

A non-repeating directed path has length at most |G.V|.

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

theorem indeg_ge_one_of_not_source (G : CFGraph) (O : CFOrientation G) (v : G.V) : ¬is_source G O v → indeg G O v ≥ 1

Vertices that are not sources must have at least one incoming edge.

theorem indeg_minus_one_nonneg_of_not_source (G : CFGraph) (O : CFOrientation G) (v : G.V) : ¬is_source G O v → 0 ≤ ↑(indeg G O v) - 1

For vertices that are not sources, indegree - 1 is non-negative.

theorem subset_source (G : CFGraph) (O : CFOrientation G) (S : Finset G.V) : S.Nonempty → is_acyclic G O → ∃ v ∈ S, ∀ w ∈ S, flow O w v = 0

In an acyclic orientation, every nonempty subset of vertices contains a vertex with no incoming flow from within the subset (a relative source).

theorem acyclic_has_source (G : CFGraph) (O : CFOrientation G) : is_acyclic G O → ∃ (v : G.V), is_source G O v

Lemma: A non-empty graph with an acyclic orientation must have at least one source.

theorem is_source_of_unique_source {G : CFGraph} (O : CFOrientation G) {q : G.V} (h_acyclic : is_acyclic G O) (h_unique_source : ∀ (w : G.V), is_source G O w → w = q) : is_source G O q

If every source of an acyclic orientation must equal q, then q is indeed a source.

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)

theorem source_of_acyclic_with_unique_source {G : CFGraph} {O : CFOrientation G} {q : G.V} (hO : acyclic_with_unique_source G O q) : is_source G O q

In an acyclic orientation with unique source q, the vertex q is a source.

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 orientation_to_config_indeg (G : CFGraph) (O : CFOrientation G) (q : G.V) (hO : acyclic_with_unique_source G O q) (v : G.V) : (orientation_to_config G O q hO).vertex_degree v = if v = q then 0 else ↑(indeg G O v) - 1

Lemma: CFOrientation to config preserves indegrees

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 sum_filter_eq_map (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)] : ∑ v : G.V, (Multiset.filter (crit v) M).card = (Multiset.map (fun (e : G.V × G.V) => {v : G.V | crit v e}.card) M).sum

Helper lemma to simplify handshking argument. Is something like this already in Mathlib somewhere?

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 helper_config_to_orientation_unique (G : CFGraph) (q : G.V) (c : Config G q) (O₁ O₂ : CFOrientation G) (hO₁ : acyclic_with_unique_source G O₁ q) (hO₂ : acyclic_with_unique_source G O₂ q) (h_eq₁ : orientation_to_config G O₁ q hO₁ = c) (h_eq₂ : orientation_to_config G O₂ q hO₂ = c) : O₁ = O₂

Lemma proving uniqueness of orientations giving same config

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.

theorem ordiv_q_reduced {G : CFGraph} (O : CFOrientation G) {q : G.V} (hO : acyclic_with_unique_source G O q) : q_reduced G q (ordiv G O)

The orientation divisor $D(\mathcal{O})$ of an acyclic orientation with unique source $q$ is $q$-reduced. Together with ordiv_unwinnable, this proves [Corry-Perkinson], Proposition 4.11.

theorem helper_orientation_config_superstable (G : CFGraph) (O : CFOrientation G) (q : G.V) (hO : acyclic_with_unique_source G O q) : superstable G q (orientation_to_config G O q hO)

The configuration associated to an acyclic orientation with unique source $q$ is superstable.

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 flow_reverse {G : CFGraph} (O : CFOrientation G) (v w : G.V) : flow (CFOrientation.reverse G O) v w = flow O w v

The flow of the reverse orientation $\overline{\mathcal{O}}$ from $v$ to $w$ equals the flow of $\mathcal{O}$ from $w$ to $v$.

theorem indeg_reverse_eq_outdeg (G : CFGraph) (O : CFOrientation G) (v : G.V) : indeg G (CFOrientation.reverse G O) v = outdeg G O v

The indegree of $v$ in the reverse orientation $\overline{\mathcal{O}}$ equals the outdegree of $v$ in $\mathcal{O}$.

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 edge_endpoints_distinct (G : CFGraph) (e : G.V × G.V) (he : e ∈ G.edges) : e.1 ≠ e.2

Helper lemma: In a loopless graph, each edge has distinct endpoints

theorem edge_incident_vertices_count (G : CFGraph) (e : G.V × G.V) (he : e ∈ G.edges) : {v : G.V | e.1 = v ∨ e.2 = v}.card = 2

Helper lemma: Each edge is incident to exactly two vertices

theorem map_inc_eq_map_two_nat (G : CFGraph) : (Multiset.map (fun (e : G.V × G.V) => {v : G.V | e.1 = v ∨ e.2 = v}.card) G.edges).sum = 2 * G.edges.card

Helper lemma: Summing mapped incidence counts equals summing constant 2 (Nat version).

theorem degree_eq_total_flow {T : Type u_1} [DecidableEq T] [Fintype T] (S : Multiset (T × T)) (v : T) : (∀ e ∈ S, e.1 ≠ e.2) → ∑ u : T, (Multiset.filter (fun (e : T × T) => e = (v, u) ∨ e = (u, v)) S).card = (Multiset.filter (fun (e : T × T) => e.1 = v ∨ e.2 = v) S).card

Helper lemma to rewrite (in-)degree in terms of edge counts from each direction. This proof is quite clunky, and I suspect it can be simplified.

theorem sum_num_edges_eq_filter_count (G : CFGraph) (v : G.V) : ∑ u : G.V, num_edges G v u = (Multiset.filter (fun (e : G.V × G.V) => e.1 = v ∨ e.2 = v) G.edges).card

theorem helper_sum_vertex_degrees (G : CFGraph) : ∑ v : G.V, vertex_degree 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 G.V} \deg(v) = 2 \cdot #(\text{edges of }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)

@[simp]

theorem count_of_multiset_of_count {T : Type u_1} [DecidableEq T] [Fintype T] (f : T → ℕ) (e : T) : Multiset.count e (multiset_of_count f) = f e

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) ⋯ ⋯

theorem dp_dec {G : CFGraph} {q : G.V} {c : Config G q} (L : burn_list G c) (h_full : ∀ (v : G.V), v ∈ L.list) (p : DirectedPath (burn_orientation L h_full)) : List.IsChain (fun (x1 x2 : ℕ) => x1 > x2) (List.map (fun (v : G.V) => List.idxOf v L.list) p.vertices)

Along any directed path in burn_orientation L, the positions of vertices in the burn list are strictly decreasing. This is the key lemma for proving acyclicity.

theorem burn_nodup {G : CFGraph} {q : G.V} {c : Config G q} (L : burn_list G c) (h_full : ∀ (v : G.V), v ∈ L.list) (p : DirectedPath (burn_orientation L h_full)) : p.vertices.Nodup

Every directed path in burn_orientation L has no repeated vertices.

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

The orientation constructed from a complete burn list is acyclic.

theorem burn_unique_source {G : CFGraph} {q : G.V} {c : Config G q} (L : burn_list G c) (h_full : ∀ (v : G.V), v ∈ L.list) (w : G.V) : is_source G (burn_orientation L h_full) w → w = q

The orientation constructed from a complete burn list has $q$ as its unique source.

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

The orientation constructed from a complete burn list is acyclic with unique source q.

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

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