The effective-difference lemma

For a connected graph of genus g ≥ 2, every degree-zero divisor class γ is the difference F - E of two effective divisors E, F of degree g - 1.

Equivalently, the two effective loci satisfy W_{g-1} ∩ (W_{g-1} - γ) ≠ ∅ in the finite graph Jacobian. The formulation below is purely in terms of divisors and linear equivalence.

Proof sketch

Write K for canonicalDivisor G and g for genus G.

1. rank G γ ≥ -1 always, and g ≥ 2 forces -1 ≥ 1 - g, so rank G γ ≥ 1 - g. Since deg γ = 0 = (g - 1) + (1 - g), Riemann--Roch (rank_ge_iff_exists_effective_canonical_complement) turns this rank bound into an effective representative M of K - γ; deg M = 2g - 2.
2. Split M into effective E, F* with deg E = deg F* = g - 1 (effective_divisor_decomposition, already in ChipFiringWithLean.Basic).
3. F* is effective, hence winnable, so by the degree-(g-1) self-duality (degree_genus_sub_one_winnable_iff_complement_winnable) its canonical complement K - F* is winnable too; let F be an effective representative.
4. F - E ~ (K - F*) - E = K - (E + F*) = K - M ~ K - (K - γ) = γ.

theorem Utilities.exists_effective_difference_of_deg_zero {G : CFGraph} (hG : graphConnected G) (hg : G.genus ≥ 2) (γ : CFDiv G) (hγ : CFDiv.degree γ = 0) : ∃ (E : CFDiv G) (F : CFDiv G), effective E ∧ effective F ∧ CFDiv.degree E = G.genus - 1 ∧ CFDiv.degree F = G.genus - 1 ∧ linearEquiv G (F - E) γ

Effective-difference lemma. On a connected graph G of genus g ≥ 2, every degree-zero divisor class γ is the difference F - E of two effective divisors E, F of degree g - 1.