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 its canonical $q$-reduced representative is qReducedConfig h_conn q D - q, with qReducedConfig h_conn q D maximal superstable (maximal_unwinnable_char).
• Every maximal unwinnable divisor has degree $g - 1$ (maximal_unwinnable_deg).

noncomputable def qReducedRep {G : CFGraph} (h_conn : graph_connected G) (q : G.V) (D : CFDiv G) : CFDiv G

The chosen unique q-reduced representative of the linear equivalence class of D.

Equations

• qReducedRep h_conn q D = Classical.choose ⋯

noncomputable def qReducedConfig {G : CFGraph} (h_conn : graph_connected G) (q : G.V) (D : CFDiv G) : Config G q

The configuration obtained from the canonical q-reduced representative of D by zeroing out the chips at q.

Equations

• qReducedConfig h_conn q D = toConfig { D := qReducedRep h_conn q D, h_eff := ⋯ }

theorem winnable_of_deg_ge_genus {G : CFGraph} (h_conn : graph_connected G) (D : CFDiv G) : deg D ≥ genus G → winnable G D

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

theorem maximal_unwinnable_char {G : CFGraph} (h_conn : graph_connected G) (q : G.V) (D : CFDiv G) : maximal_unwinnable G D ↔ maximal_superstable G (qReducedConfig h_conn q D) ∧ qReducedRep h_conn q D = (qReducedConfig h_conn q D).vertex_degree - one_chip q

A divisor $D$ is maximal unwinnable if and only if its canonical q-reduced representative is qReducedConfig h_conn q D - q, with qReducedConfig h_conn q D maximal superstable. This is [Corry-Perkinson], Corollary 4.9(2), in canonical form.

theorem superstable_and_maximal_unwinnable {G : CFGraph} (h_conn : graph_connected G) (q : G.V) (c : Config G q) (D : CFDiv G) : (superstable G q c → (maximal_superstable G c ↔ config_degree c = genus G)) ∧ (maximal_unwinnable G D ↔ maximal_superstable G (qReducedConfig h_conn q D) ∧ qReducedRep h_conn q D = (qReducedConfig h_conn q D).vertex_degree - one_chip q)

Combined characterization: the degree criterion for maximal superstable configurations and the canonical characterization of maximal unwinnable divisors, packaged together.

theorem maximal_unwinnable_deg {G : CFGraph} (h_conn : graph_connected G) (D : CFDiv G) : maximal_unwinnable G D → deg D = genus G - 1

A maximal unwinnable divisor has degree $g - 1$, computed from its canonical q-reduced representative and canonical configuration. This is [Corry-Perkinson], Corollary 4.9(4).

theorem acyclic_orientation_maximal_unwinnable_correspondence_and_degree {G : CFGraph} (h_conn : graph_connected G) (q : G.V) : (Function.Injective fun (O : { O : CFOrientation G // is_acyclic G O ∧ is_source G O q }) (v : G.V) => indeg G (↑O) v - if v = q then 1 else 0) ∧ ∀ (D : CFDiv G), 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 {G : CFGraph} (h_conn : graph_connected G) (D : CFDiv G) : 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)$.