Automatic submodularity in the two-vertex same-factor wedge exception

The genus-one Riemann--Roch rank profile leaves no negative marked second difference once the marked wedge factor has only its attachment and one other vertex. This is the converse to the obstruction in SameFactorWedgeSubmodularity.

theorem Bananas.allSubmodular_same_leftFactor_of_card_eq_two (G H : CFGraph) (x u : G.V) (y : H.V) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hCard : Fintype.card G.V = 2) (hxu : x ≠ u) : AllSubmodular (mark (Utilities.vertexWedge G H x y) (Sum.inl x) (Sum.inl u))

The intrinsic two-vertex same-factor wedge exception is automatically submodular. The proof is just genus-one Riemann--Roch on the left factor and the exact wedge rank criterion.