Genus-four rank one across a one-vertex cut

The two structural alternatives used by the finite genus-four cut checker are entirely graph-theoretic. Two genus-two factors glue with one chip saved; a genus-three factor and a pointed rigid genus-one factor glue without adding a chip. This module keeps those statements in the public gluing layer.

theorem Utilities.BNExists_vertexWedge_rankOneDegreeThree_of_genus_two_two (G : CFGraph) (H : CFGraph) (hG : graphConnected G) (hH : graphConnected H) (hGenusG : G.genus = 2) (hGenusH : H.genus = 2) (x : G.V) (y : H.V) : BNExists (vertexWedge G H x y) 1 3

Two connected genus-two factors carry a degree-three pencil on their vertex wedge.

theorem Utilities.OneVertexCut.BNExists_rankOneDegreeThree_of_genus_two_two {K : CFGraph} (cut : OneVertexCut K) (hK : graphConnected K) (hLeftGenus : cut.leftGraph.genus = 2) (hRightGenus : cut.rightGraph.genus = 2) : BNExists K 1 3

A connected graph split into two genus-two induced factors carries a degree-three rank-one divisor.

theorem Utilities.OneVertexCut.BNExists_rankOneDegreeThree_of_left_three_right_rigid_one {K : CFGraph} (cut : OneVertexCut K) (hK : graphConnected K) (hLeftGenus : cut.leftGraph.genus = 3) (hRightRigid : PointedGenusOneRigid cut.rightGraph cut.rightGlue) : BNExists K 1 3

A connected genus-three left factor and a pointed rigid genus-one right factor give the ambient degree-three pencil.

theorem Utilities.OneVertexCut.BNExists_rankOneDegreeThree_of_left_rigid_one_right_three {K : CFGraph} (cut : OneVertexCut K) (hK : graphConnected K) (hLeftRigid : PointedGenusOneRigid cut.leftGraph cut.leftGlue) (hRightGenus : cut.rightGraph.genus = 3) : BNExists K 1 3

Symmetric (1,3) form, obtained by exchanging the two sides.