Configurations and superstable configurations #
Fix a vertex $q \in V(G)$. A configuration (Config G q) is a nonnegative integer assignment
to the vertices $V(G) \setminus \{q\}$, extended by zero at $q$. This corresponds to what
Corry-Perkinson call a nonnegative configuration; we use "configuration"
to mean "nonnegative configuration" throughout this library.
A configuration $c$ is superstable if for every nonempty $S \subseteq V(G) \setminus \{q\}$, some vertex in $S$ has fewer chips than its out-degree to $V(G) \setminus S$. Equivalently, the associated divisor is $q$-reduced. A maximal superstable configuration is one that is not dominated by any other superstable configuration.
The set outdeg_S G q S v counts edges from $v$ to vertices outside $S$, and is the
relevant threshold for the superstability condition.
Sources:
- Corry-Perkinson, Definition 2.9.
- Corry-Perkinson, Definition 3.12.
A configuration on $G$ with respect to distinguished vertex $q$ is a nonnegative integer assignment to all vertices, with the convention that $q$ holds zero chips. This is what Corry-Perkinson call a nonnegative configuration.
See: Corry-Perkinson, Definition 2.9.
- vertex_degree : CFDiv G
The divisor representing the chip count at each vertex.
The distinguished vertex $q$ has no chips.
All chip counts are nonnegative.
Instances For
The degree of a configuration is the sum of all values away from $q$: $$ \deg(c) = \sum_{v \in V(G)\setminus\{q\}} c(v). $$ Since $c(q)=0$, this is implemented as the degree of the underlying divisor.
Equations
Instances For
Two configurations are equal if and only if their underlying divisors agree.
Shifting the prescribed degree by $k$ adds $k$ chips at $q$.
The divisor $c-q$ has degree $\deg(c)-1$.
Equations
- instPartialOrderConfig = { le := fun (c₁ c₂ : Config G q) => c₁.vertex_degree ≤ c₂.vertex_degree, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }
Two configurations are equal if one is pointwise bounded above by the other and they have the same degree.
The out-degree of a vertex $v$ with respect to a set $S$.
This is the number of edges from $v$ to vertices outside $S$, and is used to define the superstability condition.
Equations
- outdeg_S G q S v = ∑ w ∈ Finset.univ \ S, ↑(num_edges G v w)
Instances For
A configuration $c$ is superstable if for every nonempty $S \subseteq V(G) \setminus \{q\}$, some vertex in $S$ has fewer chips than its out-degree to $V(G) \setminus S$.
See: Corry-Perkinson, Definition 3.12.
Equations
- superstable G q c = ∀ S ⊆ Vtilde q, S.Nonempty → ∃ v ∈ S, c.vertex_degree v < outdeg_S G q S v
Instances For
A configuration $c$ is superstable if and only if toDiv d c is $q$-reduced,
for any prescribed degree $d$.
See: Corry-Perkinson, Remark 3.14.
The canonical configuration of a $q$-reduced divisor is superstable.
A maximal superstable configuration is not strictly dominated by any other superstable configuration.
Equations
- maximal_superstable G c = (superstable G q c ∧ ∀ (c' : Config G q), superstable G q c' → c ≤ c' → c' = c)
Instances For
Subtracting a chip at $q$ from a maximal superstable configuration gives an unwinnable divisor.
Burn lists and Dhar's burning algorithm #
A burn list for a configuration $c$ is an ordered list of distinct vertices ending at $q$.
The list is stored in reverse burn order: starting from $[q]$, each new burnable vertex is
prepended to the list. A vertex is burnable when its number of chips is less than its
out-degree into the vertices that have already burned. The key property is that a
configuration is superstable if and only if a complete burn list, one containing all
vertices, exists (superstable_burn_list).
The burn_flow function extracts an orientation from a burn list by directing each edge
toward the vertex that appears earlier in the list. This is used to construct the bijection
between maximal superstable configurations and acyclic orientations with unique source $q$
(see Orientation.lean).
A burn list for a configuration $c$ is a list $[v_1,v_2,\ldots,v_n,q]$ of distinct vertices ending at $q$, stored in reverse burn order.
For each $i$, let $$ S_i = V(G) \setminus \{v_{i+1},\ldots,v_n,q\}. $$ Then $v_i \in S_i$, and the out-degree of $v_i$ with respect to $S_i$, equivalently the number of edges from $v_i$ to the later vertices $\{v_{i+1},\ldots,v_n,q\}$, is greater than the number of chips at $v_i$.
Equations
- is_burn_list G c [] = False
- is_burn_list G c [x] = (x = q)
- is_burn_list G c (v :: w :: rest) = (outdeg_S G q (Finset.univ \ (w :: rest).toFinset) v > c.vertex_degree v ∧ ¬(w :: rest).contains v = true ∧ is_burn_list G c (w :: rest))
Instances For
A superstable configuration admits a complete burn list containing every vertex of $G$. This is the key output of Dhar's burning algorithm: in a superstable configuration, the whole graph burns.
The orientation induced by a burn list: for each edge $(u,v)$, direct it from $u$ to $v$ (i.e. assign nonzero flow) if $u$ appears in the list and $v$ appears before $u$. In other words, the orientation indicates the direction of the spreading fire in Dhar's burning algorithm.
Equations
Instances For
The burn_flow of a complete burn list is a valid orientation: for every edge
$\{u,v\}$, exactly num_edges G u v units of flow are directed in one of the two
directions.
For any vertex $v \ne q$ in a burn list, the in-flow into $v$ exceeds the number of chips at $v$. This is the key inequality used to construct the acyclic orientation from a maximal superstable configuration.