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 ⋯

theorem qReducedRep_spec {G : CFGraph} (h_conn : graph_connected G) (q : G.V) (D : CFDiv G) : linear_equiv G D (qReducedRep h_conn q D) ∧ q_reduced G q (qReducedRep h_conn q D)

The canonical representative is linearly equivalent to D and q-reduced.

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 qReducedConfig_superstable {G : CFGraph} (h_conn : graph_connected G) (q : G.V) (D : CFDiv G) : superstable G q (qReducedConfig h_conn q D)

The canonical configuration attached to D is superstable.

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

Every divisor $D$ is linearly equivalent to qReducedConfig h_conn q D + k·q for some integer k; in particular, it is linearly equivalent to c + k·q for a superstable configuration c.

theorem superstable_of_divisor_negative_k (G : CFGraph) (q : G.V) (D : CFDiv G) : ¬winnable G D → ∀ (c : Config G 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 (G : CFGraph) (q : G.V) (D : CFDiv G) : 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 {G : CFGraph} {q : G.V} (c : Config G 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 (G : CFGraph) (q : G.V) (D : CFDiv G) (c : Config G 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 and q-reduced, then any configuration c satisfying D = toDiv (deg D) c must realize D as c - q. This is the q-reduced core of [Corry-Perkinson], Corollary 4.9(2), "only if" direction.

theorem helper_superstable_degree_bound (G : CFGraph) (q : G.V) (c : Config G q) : superstable G q c → config_degree c ≤ genus G

Lemma: Superstable configuration degree is bounded by genus

theorem helper_degree_g_implies_maximal (G : CFGraph) (q : G.V) (c : Config G 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 (G : CFGraph) (q : G.V) (c : Config G 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 {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 helper_maximal_superstable_chip_winnable_exact {G : CFGraph} (h_conn : graph_connected G) (q : G.V) (c' : Config G q) : maximal_superstable G c' → ∀ (v : G.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_q_reduced_toConfig_form {G : CFGraph} (q : G.V) (D : CFDiv G) (h_max : maximal_unwinnable G D) (h_qred : q_reduced G q D) : D = (toConfig { D := D, h_eff := ⋯ }).vertex_degree - one_chip q

A maximal unwinnable q-reduced divisor is the canonical toConfig form minus one chip at q.

theorem maximal_unwinnable_of_maximal_superstable_form {G : CFGraph} (h_conn : graph_connected G) (q : G.V) (c : Config G q) : maximal_superstable G c → maximal_unwinnable G (c.vertex_degree - one_chip q)

A divisor of the form c - q is maximal unwinnable when c is maximal superstable.

theorem maximal_unwinnable_q_reduced_toConfig_iff {G : CFGraph} (h_conn : graph_connected G) (q : G.V) (D : CFDiv G) (h_qred : q_reduced G q D) : maximal_unwinnable G D ↔ maximal_superstable G (toConfig { D := D, h_eff := ⋯ }) ∧ D = (toConfig { D := D, h_eff := ⋯ }).vertex_degree - one_chip q

For a q-reduced divisor, maximal unwinnability is equivalent to the maximal superstability of its canonical configuration together with the canonical c - q form.

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)$.