A rigid genus-one wedge on a genus-three graph

The canonical slack-pair construction supplies a degree-three divisor D on the genus-three factor with both rank one and D - 2(x) winnable. The exact rigid-wedge criterion therefore carries that same divisor across an attached genus-one cycle without adding chips.

The theorem uses the established MarkedGraphs namespace for API compatibility.

theorem MarkedGraphs.BNExists_vertexWedge_rankOneDegreeThree_of_genus_three (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (hG : graphConnected G) (hGenusG : G.genus = 3) (hH : Utilities.PointedGenusOneRigid H y) : Utilities.BNExists (Utilities.vertexWedge G H x y) 1 3

A rigid genus-one block attached to a connected genus-three base carries the base's degree-three pencil without adding any chips on the genus-one factor.