Maximal superstable configurations and maximal unwinnable divisors

This section establishes the correspondence between maximal superstable configurations and maximal unwinnable divisors:

• A superstable configuration $c$ is maximal if and only if $\deg(c) = g$ (maximal_superstable_config_prop).
• A divisor $D$ is maximal unwinnable if and only if it is linearly equivalent to $c - q$ for some maximal superstable $c$ (maximal_unwinnable_char).
• Every maximal unwinnable divisor has degree $g - 1$ (maximal_unwinnable_deg).

theorem superstable_of_divisor {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (h_conn : graph_connected G) (q : V) (D : CFDiv V) : ∃ (c : Config V q) (k : ℤ), linear_equiv G D (c.vertex_degree + k • one_chip q) ∧ superstable G q c

Every divisor $D$ is linearly equivalent to $c + k \cdot q$ for some superstable configuration $c$ and integer $k$.

theorem superstable_of_divisor_negative_k {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (q : V) (D : CFDiv V) : ¬winnable G D → ∀ (c : Config V q) (k : ℤ), linear_equiv G D (c.vertex_degree + k • one_chip q) → superstable G q c → k < 0

If $D$ is unwinnable and $D \sim c + k \cdot q$ for a superstable $c$, then $k < 0$.

theorem maximal_unwinnable_q_reduced_chips_at_q {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (q : V) (D : CFDiv V) : maximal_unwinnable G D → q_reduced G q D → D q = -1

If $D$ is maximal unwinnable and $q$-reduced, then $D(q) = -1$.

theorem degree_max_superstable {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} {q : V} (c : Config V q) (h_max : maximal_superstable G c) : config_degree c = genus G

A maximal superstable configuration has degree equal to the genus. This is [Corry-Perkinson], Corollary 4.9(1), "only if" direction.

theorem maximal_unwinnable_q_reduced_form {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (q : V) (D : CFDiv V) (c : Config V q) : maximal_unwinnable G D → q_reduced G q D → D = toDiv (deg D) c → D = c.vertex_degree - one_chip q

If $D$ is maximal unwinnable, $q$-reduced, and equals toDiv (deg D) c, then $D = c - q$. This is [Corry-Perkinson], Corollary 4.9(2), "only if" direction.

theorem helper_superstable_degree_bound {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (q : V) (c : Config V q) : superstable G q c → config_degree c ≤ genus G

Lemma: Superstable configuration degree is bounded by genus

theorem helper_maximal_superstable_degree_lower_bound {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (q : V) (c : Config V q) : superstable G q c → maximal_superstable G c → config_degree c ≥ genus G

A maximal superstable configuration has degree at least the genus. Combined with helper_superstable_degree_bound, this gives degree_max_superstable.

theorem helper_degree_g_implies_maximal {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (q : V) (c : Config V q) : superstable G q c → config_degree c = genus G → maximal_superstable G c

Lemma: If a superstable configuration has degree equal to g, it is maximal [Corry-Perkinson], Corollary 4.9(1), "if" direction.

theorem maximal_superstable_config_prop {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (q : V) (c : Config V q) : superstable G q c → (maximal_superstable G c ↔ config_degree c = genus G)

A superstable configuration is maximal if and only if its degree equals the genus. This is [Corry-Perkinson], Corollary 4.9(1).

theorem winnable_of_deg_ge_genus {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (h_conn : graph_connected G) (D : CFDiv V) : deg D ≥ genus G → winnable G D

A divisor of degree at least $g$ is winnable.

theorem helper_maximal_superstable_chip_winnable_exact {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (h_conn : graph_connected G) (q : V) (c' : Config V q) : maximal_superstable G c' → ∀ (v : V), winnable G (c'.vertex_degree - one_chip q + one_chip v)

Lemma: Adding a chip anywhere to c'-q makes it winnable when c' is maximal superstable

theorem maximal_unwinnable_char {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (h_conn : graph_connected G) (q : V) (D : CFDiv V) : maximal_unwinnable G D ↔ ∃ (c : Config V q), maximal_superstable G c ∧ ∃ (D' : CFDiv V), q_reduced G q D' ∧ linear_equiv G D D' ∧ D' = c.vertex_degree - one_chip q

A divisor $D$ is maximal unwinnable if and only if it is linearly equivalent to $c - q$ for some maximal superstable configuration $c$. This is [Corry-Perkinson], Corollary 4.9(2).

theorem superstable_and_maximal_unwinnable {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (h_conn : graph_connected G) (q : V) (c : Config V q) (D : CFDiv V) : (superstable G q c → (maximal_superstable G c ↔ config_degree c = genus G)) ∧ (maximal_unwinnable G D ↔ ∃ (c : Config V q), maximal_superstable G c ∧ ∃ (D' : CFDiv V), q_reduced G q D' ∧ linear_equiv G D D' ∧ D' = fun (v : V) => c.vertex_degree v - if v = q then 1 else 0)

Combined characterization: maximal_superstable_config_prop and maximal_unwinnable_char packaged together.

theorem maximal_unwinnable_deg {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (h_conn : graph_connected G) (D : CFDiv V) : maximal_unwinnable G D → deg D = genus G - 1

A maximal unwinnable divisor has degree $g - 1$. This is [Corry-Perkinson], Corollary 4.9(4).

theorem acyclic_orientation_maximal_unwinnable_correspondence_and_degree {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (h_conn : graph_connected G) (q : V) : (Function.Injective fun (O : { O : CFOrientation G // is_acyclic G O ∧ is_source G O q }) (v : V) => indeg G (↑O) v - if v = q then 1 else 0) ∧ ∀ (D : CFDiv V), maximal_unwinnable G D → deg D = genus G - 1

The map sending an acyclic orientation with source $q$ to its orientation divisor is injective, and every maximal unwinnable divisor has degree $g - 1$. The injectivity claim is [Corry-Perkinson], Corollary 4.9(3).

The main Riemann-Roch inequality

rank_degree_inequality establishes the strict inequality $$\deg(D) - g < r(D) - r(K_G - D),$$ which is the main step toward the Riemann-Roch theorem for graphs. The proof uses Dhar's burning algorithm to find a maximal superstable configuration dominating the configuration associated to $D - E$, then dualizes via the reverse orientation to bound $r(K_G - D)$.

theorem rank_degree_inequality {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (h_conn : graph_connected G) (D : CFDiv V) : deg D - genus G < rank G D - rank G (canonical_divisor G - D)

The strict Riemann-Roch inequality: $\deg(D) - g < r(D) - r(K_G - D)$.