Riemann--Roch duality for transmission rows

For a transmission witness, every marked twist has known degree. Riemann--Roch therefore converts its rank inequality into an equivalent lower bound for the canonical complement. This file packages that conversion without yet using any ASP-specific simplification of the complementary slipface expression.

theorem Utilities.transmission_twist_rank_rr {G : CFGraph} (hconn : graphConnected G) {u v : G.V} {τ : AspPerm} {D : CFDiv G} (h : SatisfiesTransmission G u v τ D) (a b : ℤ) : rank G (D + a • oneChip u - b • oneChip v) - rank G (canonicalDivisor G - (D + a • oneChip u - b • oneChip v)) = τ.χ + a - b + 1

Exact Riemann--Roch relation for a marked twist of a transmission witness.

theorem Utilities.transmission_twist_rank_eq_complement_rank {G : CFGraph} (hconn : graphConnected G) {u v : G.V} {τ : AspPerm} {D : CFDiv G} (h : SatisfiesTransmission G u v τ D) (a b : ℤ) : rank G (D + a • oneChip u - b • oneChip v) = rank G (canonicalDivisor G - (D + a • oneChip u - b • oneChip v)) + τ.χ + a - b + 1

Solved form of the marked Riemann--Roch relation.

theorem Utilities.canonical_complement_rank_ge_of_satisfiesTransmission {G : CFGraph} (hconn : graphConnected G) {u v : G.V} {τ : AspPerm} {D : CFDiv G} (h : SatisfiesTransmission G u v τ D) (a b : ℤ) : rank G (canonicalDivisor G - (D + a • oneChip u - b • oneChip v)) ≥ τ.s.func (a + 1) b - τ.χ - a + b - 2

The transmission row inequality implies the corresponding canonical complement lower bound.

theorem Utilities.transmission_row_iff_canonical_complement_row {G : CFGraph} (hconn : graphConnected G) {u v : G.V} {τ : AspPerm} {D : CFDiv G} (hDegree : CFDiv.degree D = G.genus + τ.χ) (a b : ℤ) : TransmissionInequality G u v τ D a b ↔ rank G (canonicalDivisor G - (D + a • oneChip u - b • oneChip v)) ≥ τ.s.func (a + 1) b - τ.χ - a + b - 2

For a transmission witness, the original row lower bound is equivalent to the Riemann--Roch translated lower bound on its canonical complement.

theorem Utilities.canonical_complement_rows_of_satisfiesTransmission {G : CFGraph} (hconn : graphConnected G) {u v : G.V} {τ : AspPerm} {D : CFDiv G} (h : SatisfiesTransmission G u v τ D) (a b : ℤ) : rank G (canonicalDivisor G - (D + a • oneChip u - b • oneChip v)) ≥ τ.s.func (a + 1) b - τ.χ - a + b - 2

Package the dual row inequalities for all lattice points.