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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) : Type

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 (V × V)

  The set of directed edges in the orientation

• count_preserving (v w : 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 : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (O : CFOrientation G) (u v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (O : CFOrientation G) (u v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (O1 O2 : CFOrientation G) : O1 = O2 ↔ ∀ (u v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (f : V × V → ℕ) : ∑ u : V, ∑ v : V, f (u, v) = ∑ e : V × V, f e

Helper lema for the count below.

theorem card_directed_edges_eq_card_edges {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (O : CFOrientation G) (v : V) : ℕ

Number of edges directed into a vertex under an orientation

Equations

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

theorem indeg_eq_sum_flow {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (O : CFOrientation G) (v : V) : indeg G O v = ∑ w : V, flow O w v

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

def outdeg {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (O : CFOrientation G) (v : V) : ℕ

Number of edges directed out of a vertex under an orientation

Equations

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

def is_source {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (O : CFOrientation G) (v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (O : CFOrientation G) (v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (O : CFOrientation G) (u v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (O : CFOrientation G) : Type

A directed path in a graph under an orientation

• vertices : List 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} {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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} {O : CFOrientation G} (p : DirectedPath O) : non_repeating p → p.vertices.length ≤ Fintype.card V

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

def is_acyclic {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (O : CFOrientation G) (v : V) : Finset 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 : V | Relation.TransGen (fun (a b : V) => directed_edge G O a b) x v}

noncomputable def vertexLevelMeasure {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (O : CFOrientation G) (v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (O : CFOrientation G) (v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (O : CFOrientation G) (v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (O : CFOrientation G) (S : Finset 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (O : CFOrientation G) : is_acyclic G O → ∃ (v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (O : CFOrientation G) {q : V} (h_acyclic : is_acyclic G O) (h_unique_source : ∀ (w : 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 config_of_source {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} {O : CFOrientation G} {q : V} (h_acyclic : is_acyclic G O) (h_unique_source : ∀ (w : V), is_source G O w → w = q) : Config V 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 h_acyclic h_unique_source = { vertex_degree := fun (v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (O : CFOrientation G) : CFDiv V

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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (O : CFOrientation G) {q : V} (h_acyclic : is_acyclic G O) (h_unique_source : ∀ (w : V), is_source G O w → w = q) : q_eff_div V q

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

Equations

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

def orientation_to_config {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (O : CFOrientation G) (q : V) (h_acyclic : is_acyclic G O) (h_unique_source : ∀ (w : V), is_source G O w → w = q) : Config V 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 h_acyclic h_unique_source = config_of_source h_acyclic h_unique_source

theorem orientation_to_config_indeg {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (O : CFOrientation G) (q : V) (h_acyclic : is_acyclic G O) (h_unique_source : ∀ (w : V), is_source G O w → w = q) (v : V) : (orientation_to_config G O q h_acyclic h_unique_source).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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (O : CFOrientation G) {q : V} (h_acyclic : is_acyclic G O) (h_unique_source : ∀ (w : V), is_source G O w → w = q) : orientation_to_config G O q h_acyclic h_unique_source = toConfig (orqed O h_acyclic h_unique_source)

Compatibility between configurations and divisors from an orientation

theorem sum_filter_eq_map {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (M : Multiset (V × V)) (crit : V → V × V → Prop) [(v : V) → (e : V × V) → Decidable (crit v e)] : ∑ v : V, (Multiset.filter (crit v) M).card = (Multiset.map (fun (e : V × V) => {v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (O O' : CFOrientation G) : is_acyclic G O → is_acyclic G O' → (∀ (v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (q : V) (c : Config V q) (h_super : superstable G q c) (h_max : maximal_superstable G c) (O₁ O₂ : CFOrientation G) (h_acyc₁ : is_acyclic G O₁) (h_acyc₂ : is_acyclic G O₂) (h_src₁ : is_source G O₁ q) (h_src₂ : is_source G O₂ q) (h_unique_source₁ : ∀ (w : V), is_source G O₁ w → w = q) (h_unique_source₂ : ∀ (w : V), is_source G O₂ w → w = q) (h_eq₁ : orientation_to_config G O₁ q h_acyc₁ h_unique_source₁ = c) (h_eq₂ : orientation_to_config G O₂ q h_acyc₂ h_unique_source₂ = c) : O₁ = O₂

Lemma proving uniqueness of orientations giving same config

theorem degree_ordiv {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (O : CFOrientation G) {q : V} (h_acyclic : is_acyclic G O) (h_unique_source : ∀ (w : V), is_source G O w → w = q) : config_degree (orientation_to_config G O q h_acyclic h_unique_source) = genus G

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

theorem ordiv_unwinnable {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (O : CFOrientation G) {q : V} (h_acyclic : is_acyclic G O) (h_unique_source : ∀ (w : V), is_source G O w → w = 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (O : CFOrientation G) (q : V) (h_acyc : is_acyclic G O) (h_unique_source : ∀ (w : V), is_source G O w → w = q) : superstable G q (orientation_to_config G O q h_acyc h_unique_source)

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 V} \deg(v) = 2|E|$, and its corollary that $\deg(K_G) = 2g - 2$ (degree_of_canonical_divisor).

def canonical_divisor {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) : CFDiv V

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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (O : CFOrientation G) (v w : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (O : CFOrientation G) (v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (e : V × 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (e : V × V) (he : e ∈ G.edges) : {v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) : (Multiset.map (fun (e : V × V) => {v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (S : Multiset (V × V)) (v : V) : (∀ e ∈ S, e.1 ≠ e.2) → ∑ u : V, (Multiset.filter (fun (e : V × V) => e = (v, u) ∨ e = (u, v)) S).card = (Multiset.filter (fun (e : V × V) => 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (v : V) : ∑ u : V, num_edges G v u = (Multiset.filter (fun (e : V × V) => e.1 = v ∨ e.2 = v) G.edges).card

theorem helper_sum_vertex_degrees {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) : ∑ v : 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 V} \deg(v) = 2 \cdot #(\text{edges of }G). ]

theorem degree_of_canonical_divisor {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) : 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 helper definitions dec and dec' formalize strictly decreasing sequences of natural numbers, and orientation_from_flow constructs a CFOrientation from an explicit flow function.

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

Create a multiset with a given count function. This seems likely to be in Mathlib already, but I didn't find it.

Equations

• multiset_of_count f = Finset.univ.val.bind fun (e : T) => Multiset.replicate (f e) e

@[simp]

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

def orientation_from_flow {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (f : V × V → ℕ) (h_count_preserving : ∀ (v w : V), f (v, w) + f (w, v) = num_edges G v w) (h_no_bidirectional : ∀ (v w : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} {q : V} {c : Config V q} (L : burn_list G c) (h_full : ∀ (v : 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 nodup_of_map_nodup (S : Type u_1) (T : Type u_2) (L : List S) (f : S → T) : (List.map f L).Nodup → L.Nodup

Utility for proving acyclicity. This is a fairly basic fact that may be in Mathlib, but I haven't found it.

def dec (L : List ℕ) : Prop

A list of natural numbers is decreasing (dec) if every element is greater than all subsequent elements.

Equations

• dec [] = True
• dec (x :: xs) = ((∀ y ∈ xs, x > y) ∧ dec xs)

theorem nodup_of_dec (L : List ℕ) (h_dec : dec L) : L.Nodup

A decreasing list has no duplicates.

def dec' (L : List ℕ) : Prop

An equivalent pairwise-consecutive formulation of dec: each element is greater than the next.

Equations

• dec' [] = True
• dec' [x] = True
• dec' (x :: y :: zs) = (x > y ∧ dec' (y :: zs))

theorem dec_iff_dec' (L : List ℕ) : dec L ↔ dec' L

The definitions dec and dec' are equivalent.

@[irreducible]

theorem dp_dec {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} {q : V} {c : Config V q} (L : burn_list G c) (h_full : ∀ (v : V), v ∈ L.list) (p : DirectedPath (burn_orientation L h_full)) : dec (List.map (fun (v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} {q : V} {c : Config V q} (L : burn_list G c) (h_full : ∀ (v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} {q : V} {c : Config V q} (L : burn_list G c) (h_full : ∀ (v : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} {q : V} {c : Config V q} (L : burn_list G c) (h_full : ∀ (v : V), v ∈ L.list) (w : 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.

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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} {q : V} {c : Config V q} (h_ss : superstable G q c) : ∃ (O : CFOrientation G) (h_acyc : is_acyclic G O) (h_unique_source : ∀ (w : V), is_source G O w → w = q), config_ge (orientation_to_config G O q h_acyc h_unique_source) c

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

theorem orientation_config_maximal {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (O : CFOrientation G) (q : V) (h_acyc : is_acyclic G O) (h_unique_source : ∀ (w : V), is_source G O w → w = q) : maximal_superstable G (orientation_to_config G O q h_acyc h_unique_source)

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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (q : V) (c : Config V q) (h_super : superstable G q c) : ∃ (c' : Config V q), maximal_superstable G c' ∧ config_ge c' c

Every superstable configuration extends to a maximal superstable configuration

theorem maximal_superstable_orientation {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (q : V) (c : Config V q) (h_max : maximal_superstable G c) : ∃ (O : CFOrientation G) (h_acyc : is_acyclic G O) (h_unique_source : ∀ (w : V), is_source G O w → w = q), orientation_to_config G O q h_acyc h_unique_source = c

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

theorem orientation_superstable_bijection {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (q : V) : let α := { O : CFOrientation G // is_acyclic G O ∧ ∀ (w : V), is_source G O w → w = q }; let β := { c : Config V 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)