Degree-specialized Riemann--Roch and winnability

For a divisor of degree g - 1 + k, graph Riemann--Roch says that the rank condition rank D ≥ k is exactly winnability of the canonical complement K - D. This is the form used repeatedly by residual-chip and common-complement arguments, where the degree bookkeeping is fixed before the rank condition is applied.

theorem Utilities.rank_ge_iff_canonical_sub_winnable_of_degree {G : CFGraph} (hG : graphConnected G) (D : CFDiv G) (k : ℤ) (hDegree : CFDiv.degree D = G.genus - 1 + k) : rank G D ≥ k ↔ winnable G (canonicalDivisor G - D)

At degree g - 1 + k, rank at least k is equivalent to winnability of the canonical complement.

theorem Utilities.rank_ge_iff_exists_effective_canonical_complement {G : CFGraph} (hG : graphConnected G) (D : CFDiv G) (k : ℤ) (hDegree : CFDiv.degree D = G.genus - 1 + k) : rank G D ≥ k ↔ ∃ (E : CFDiv G), effective E ∧ linearEquiv G (canonicalDivisor G - D) E

Effective-representative form of the degree-specialized Riemann--Roch criterion. This is convenient for residual constructions: a rank hypothesis can be destructed directly into an effective representative of K - D.

theorem Utilities.canonical_sub_rank_ge_iff_winnable_of_degree {G : CFGraph} (hG : graphConnected G) (F : CFDiv G) (k : ℤ) (hDegree : CFDiv.degree F = G.genus - 1 - k) : rank G (canonicalDivisor G - F) ≥ k ↔ winnable G F

Complementary form: if F has degree g - 1 - k, then K - F has rank at least k exactly when F is winnable.

theorem Utilities.canonical_sub_rank_ge_iff_exists_effective {G : CFGraph} (hG : graphConnected G) (F : CFDiv G) (k : ℤ) (hDegree : CFDiv.degree F = G.genus - 1 - k) : rank G (canonicalDivisor G - F) ≥ k ↔ ∃ (E : CFDiv G), effective E ∧ linearEquiv G F E

Effective-representative version of the complementary criterion.

theorem Utilities.canonical_sub_rank_ge_one_iff_winnable {G : CFGraph} (hG : graphConnected G) (F : CFDiv G) (hDegree : CFDiv.degree F = G.genus - 2) : rank G (canonicalDivisor G - F) ≥ 1 ↔ winnable G F

The rank-one canonical-complement test used in the width-two and prescribed-residual constructions.

theorem Utilities.degree_genus_sub_one_winnable_iff_complement_winnable {G : CFGraph} (hG : graphConnected G) (D : CFDiv G) (hDegree : CFDiv.degree D = G.genus - 1) : winnable G D ↔ winnable G (canonicalDivisor G - D)

The degree-g-1 case: a divisor is winnable exactly when its canonical complement is winnable.