Same-factor submodularity on a rigid genus-one wedge

The same-factor branch of Theorem 4.13 only survives when that factor has two vertices. The point is that a third vertex supplies the explicit negative rank-difference witness already used for Proposition 3.7.

theorem Bananas.pointedGenusOneRigid_of_any_vertex (G : CFGraph) (x : G.V) (hConnected : _root_.graphConnected G) (hGenus : G.genus = 1) (hCut : Utilities.TwoEdgeCutCondition G) : Utilities.PointedGenusOneRigid G x

On a bridgeless genus-one factor, pointed rigidity is available at every vertex, not merely at the wedge attachment.

theorem Bananas.card_leftFactor_le_two_of_allSubmodular (G H : CFGraph) (x u : G.V) (y : H.V) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hCut : Utilities.TwoEdgeCutCondition G) (hSub : AllSubmodular (mark (Utilities.vertexWedge G H x y) (Sum.inl x) (Sum.inl u))) : Fintype.card G.V ≤ 2

If two distinct marks lie in the left genus-one factor of a bridgeless wedge and all divisors are submodular, that factor has exactly its two marked vertices. A third vertex gives the explicit negative second difference.

theorem Bananas.same_leftFactor_marks_of_allSubmodular (G H : CFGraph) (x u v : G.V) (y : H.V) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hCut : Utilities.TwoEdgeCutCondition G) (hSub : AllSubmodular (mark (Utilities.vertexWedge G H x y) (Sum.inl u) (Sum.inl v))) : (u = x ∨ v = x) ∧ Fintype.card G.V ≤ 2

The only all-submodular marking supported on one factor of a bridgeless genus-one wedge uses the gluing vertex and a two-vertex factor.

theorem Bananas.same_leftFactor_marks_of_kGeneral (G H : CFGraph) (x u v : G.V) (y : H.V) (k : ℕ) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hCut : Utilities.TwoEdgeCutCondition G) (hK : KGeneralTransmission (mark (Utilities.vertexWedge G H x y) (Sum.inl u) (Sum.inl v)) k) : (u = x ∨ v = x) ∧ Fintype.card G.V ≤ 2

The necessary same-factor conclusion for a general-transmission wedge is just its all-submodularity component.