Right-factor form of the same-factor wedge exception

This is the factor-symmetric transport of the left-factor theorems across the explicit commutativity isomorphism for vertex wedges.

theorem Bananas.same_rightFactor_marks_of_allSubmodular (G H : CFGraph) (x : G.V) (y p q : H.V) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hCut : Utilities.TwoEdgeCutCondition H) (hSub : AllSubmodular (mark (Utilities.vertexWedge G H x y) (Utilities.wedgeRightVertex G H x y p) (Utilities.wedgeRightVertex G H x y q))) : (p = y ∨ q = y) ∧ Fintype.card H.V ≤ 2

theorem Bananas.same_rightFactor_marks_of_kGeneral (G H : CFGraph) (x : G.V) (y p q : H.V) (k : ℕ) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hCut : Utilities.TwoEdgeCutCondition H) (hK : KGeneralTransmission (mark (Utilities.vertexWedge G H x y) (Utilities.wedgeRightVertex G H x y p) (Utilities.wedgeRightVertex G H x y q)) k) : (p = y ∨ q = y) ∧ Fintype.card H.V ≤ 2

The necessary right-factor conclusion for a general-transmission wedge.

theorem Bananas.same_rightFactor_wedge_twoGeneral (G H : CFGraph) (x : G.V) (y p : H.V) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hCut : Utilities.TwoEdgeCutCondition H) (hCard : Fintype.card H.V = 2) (hpy : p ≠ y) (hSub : AllSubmodular (mark (Utilities.vertexWedge G H x y) (Utilities.wedgeRightVertex G H x y y) (Utilities.wedgeRightVertex G H x y p))) : KGeneralTransmission (mark (Utilities.vertexWedge G H x y) (Utilities.wedgeRightVertex G H x y y) (Utilities.wedgeRightVertex G H x y p)) 2

theorem Bananas.same_rightFactor_wedge_twoGeneral_of_card_eq_two (G H : CFGraph) (x : G.V) (y p : H.V) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hCut : Utilities.TwoEdgeCutCondition H) (hCard : Fintype.card H.V = 2) (hpy : p ≠ y) : KGeneralTransmission (mark (Utilities.vertexWedge G H x y) (Utilities.wedgeRightVertex G H x y y) (Utilities.wedgeRightVertex G H x y p)) 2

The two-vertex same-right-factor exception is automatically two-general; this is the commuted form of the genus-one Riemann--Roch left-factor theorem.

theorem Bananas.same_rightFactor_wedge_isTorsionOrder_two (G H : CFGraph) (x : G.V) (y p : H.V) (hH : Utilities.PointedGenusOneRigid H y) (hCut : Utilities.TwoEdgeCutCondition H) (hCard : Fintype.card H.V = 2) (hpy : p ≠ y) : IsTorsionOrder (mark (Utilities.vertexWedge G H x y) (Utilities.wedgeRightVertex G H x y y) (Utilities.wedgeRightVertex G H x y p)) 2