The period in the same-factor wedge exception

theorem Bananas.same_leftFactor_kGeneral_period_eq_two (G H : CFGraph) (x u : G.V) (y : H.V) (k : ℕ) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hCut : Utilities.TwoEdgeCutCondition G) (hCard : Fintype.card G.V = 2) (hxu : x ≠ u) (hK : KGeneralTransmission (mark (Utilities.vertexWedge G H x y) (Sum.inl x) (Sum.inl u)) k) : k = 2

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