Genus-two seeds for two-pole gluing

The two-pole compatibility problem is most naturally studied after retaining one cross-edge and contracting its separating bridge. The result is a genus-two/genus-two vertex wedge with glue vertex a. Two uniform facts hold there without any metric or combinatorial case split:

• the sum K_A + K_B of the factor canonical divisors has rank at least one;
• the four-chip glue pile has rank at least one and 4a - 2u is winnable for every vertex u of the wedge.

The second statement is the marked seed. Its proof is just the critical degree form of Riemann's inequality on whichever genus-two factor contains u. The only remaining issue after restoring the second cross-edge is to choose one seam phase compatible with the desired rank tests; that scalar problem is represented by TwoPoleProfile.lean.

theorem Utilities.TwoPole.winnable_of_degree_eq_genus (G : CFGraph) (hG : graphConnected G) (D : CFDiv G) (hDegree : CFDiv.degree D = G.genus) : winnable G D

A divisor whose degree equals the genus is winnable.

theorem Utilities.TwoPole.deg_zsmul_one_chip (G : CFGraph) (q : G.V) (n : ℤ) : CFDiv.degree (n • oneChip q) = n

Degree of an integral pile at one vertex.

theorem Utilities.TwoPole.winnable_four_pile_sub_two (G : CFGraph) (a uMark : G.V) (hG : graphConnected G) (hGenus : G.genus = 2) : winnable G (4 • oneChip a - 2 • oneChip uMark)

The local 4a - 2u lemma. On a connected genus-two graph, four chips at any anchor absorb a doubled chip at any marked vertex.

The four-chip pile on a genus-two/genus-two wedge

def Utilities.TwoPole.wedgeGluePile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : CFDiv (vertexWedge G H x y)

The four-chip pile at the common vertex of a wedge.

Equations

• Utilities.TwoPole.wedgeGluePile G H x y = Utilities.wedgeAddDivisor G H x y (4 • oneChip x) 0

theorem Utilities.TwoPole.wedgeGluePile_eq_right (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : wedgeGluePile G H x y = wedgeAddDivisor G H x y 0 (4 • oneChip y)

The glue pile has the same presentation from the right factor.

theorem Utilities.TwoPole.wedgeGluePile_sub_two_inl (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (a : G.V) : wedgeGluePile G H x y - 2 • oneChip (Sum.inl a) = wedgeAddDivisor G H x y (4 • oneChip x - 2 • oneChip a) 0

Removing a doubled left vertex from the glue pile stays on the left factor.

theorem Utilities.TwoPole.wedgeGluePile_sub_two_inr (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (b : { b : H.V // b ≠ y }) : wedgeAddDivisor G H x y 0 (4 • oneChip y) - 2 • oneChip (Sum.inr b) = wedgeAddDivisor G H x y 0 (4 • oneChip y - 2 • oneChip ↑b)

Removing a doubled strictly-right vertex from the right presentation of the glue pile stays on the right factor.

theorem Utilities.TwoPole.winnable_wedgeGluePile_sub_two (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (hG : graphConnected G) (hGenusG : G.genus = 2) (hH : graphConnected H) (hGenusH : H.genus = 2) (uMark : (vertexWedge G H x y).V) : winnable (vertexWedge G H x y) (wedgeGluePile G H x y - 2 • oneChip uMark)

The wedge 4a - 2u lemma. Four chips at the glue vertex of a genus-two/genus-two wedge absorb a doubled chip at every vertex.

theorem Utilities.TwoPole.rank_wedgeGluePile_ge_one (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (hG : graphConnected G) (hGenusG : G.genus = 2) (hH : graphConnected H) (hGenusH : H.genus = 2) : rank (vertexWedge G H x y) (wedgeGluePile G H x y) ≥ 1

Four chips at the glue vertex of a genus-two/genus-two wedge form a rank-one divisor.

The unmarked local-canonical seed

theorem Utilities.TwoPole.rank_wedge_canonicalSum_ge_one (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (hG : graphConnected G) (hGenusG : G.genus = 2) (hH : graphConnected H) (hGenusH : H.genus = 2) : rank (vertexWedge G H x y) (wedgeAddDivisor G H x y (canonicalDivisor G) (canonicalDivisor H)) ≥ 1

Unmarked K_A + K_B lemma on the one-pole model. The sum of the two factor canonical divisors has rank at least one on a wedge of connected genus-two graphs.