Canonical slack pairs

On a connected graph of genus at least three, split an effective representative of K - (x) - (y) into equal halves. Restoring the two marked chips produces complementary degree-g, rank-one divisors, each of which remains winnable after removing the marked pair.

The declarations use the established MarkedGraphs namespace for API compatibility.

def MarkedGraphs.IsSlackNearRectangleDivisor (H : CFGraph) (x y : H.V) (D : CFDiv H) : Prop

A specified divisor satisfying the slack-column near-rectangle conditions at the marked vertices: degree equal to the genus, rank at least one, and nonnegative rank after the two marked chips are removed.

Equations

• MarkedGraphs.IsSlackNearRectangleDivisor H x y D = (CFDiv.degree D = H.genus ∧ rank H D ≥ 1 ∧ rank H (D - oneChip x - oneChip y) ≥ 0)

theorem MarkedGraphs.isSlackNearRectangleDivisor_of_canonical_split (H : CFGraph) (hH : graphConnected H) (x y : H.V) (E F : CFDiv H) (hEEffective : effective E) (hFEffective : effective F) (hEDegree : CFDiv.degree E = H.genus - 2) (hSplit : linearEquiv H (canonicalDivisor H - (oneChip x + oneChip y)) (E + F)) : IsSlackNearRectangleDivisor H x y (E + oneChip x + oneChip y)

Either half of a splitting of the marked canonical residual, restored by the two marked chips, is a slack near-rectangle divisor.

theorem MarkedGraphs.exists_canonical_slack_dual_pair (H : CFGraph) (hH : graphConnected H) (hGenus : 3 ≤ H.genus) (x y : H.V) : ∃ (D₁ : CFDiv H) (D₂ : CFDiv H), IsSlackNearRectangleDivisor H x y D₁ ∧ IsSlackNearRectangleDivisor H x y D₂ ∧ linearEquiv H (D₁ + D₂) (canonicalDivisor H + oneChip x + oneChip y)

On a connected graph of genus at least three, every pair of marked vertices admits complementary slack near-rectangle divisors.