The exact order of a two-vertex bridgeless genus-one factor

A loopless genus-one graph with two vertices and no one-edge cut consists of two parallel edges. Firing either vertex therefore doubles the marked difference, while rigidity excludes order one.

theorem Bananas.twoVertexGenusOne_isTorsionOrder_two (G : CFGraph) (x u : G.V) (hRigid : Utilities.PointedGenusOneRigid G x) (hCut : Utilities.TwoEdgeCutCondition G) (hCard : Fintype.card G.V = 2) (hxu : x ≠ u) : IsTorsionOrder (mark G x u) 2

The two distinct vertices of a bridgeless two-vertex genus-one factor have marked-difference torsion of exact order two.