Symmetric period comparison on a rigid genus-two wedge

WedgeKGeneralConverse proves the period comparison after choosing an order on the two factors. This file removes that bookkeeping hypothesis by commuting the vertex wedge and swapping the marked vertices in the other case.

theorem Bananas.factor_torsionOrders_eq_of_vertexWedge_opposite_kGeneral_symmetric {G H : CFGraph} (x : G.V) (y : H.V) (u : G.V) (v : H.V) (a b k : ℕ) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hu : u ≠ x) (hv : v ≠ y) (hA : IsTorsionOrder (mark G u x) a) (hB : IsTorsionOrder (mark H y v) b) (hWCut : Utilities.TwoEdgeCutCondition (Utilities.vertexWedge G H x y)) (hWRigid : ¬linearEquiv (Utilities.vertexWedge G H x y) (oneChip (Sum.inl u) + oneChip (Utilities.wedgeRightVertex G H x y v)) (canonicalDivisor (Utilities.vertexWedge G H x y))) (hK : KGeneralTransmission (mark (Utilities.vertexWedge G H x y) (Sum.inl u) (Utilities.wedgeRightVertex G H x y v)) k) : a = b

The period comparison on an opposite-side rigid wedge is symmetric in the two factors: distinct factor marks force their exact torsion orders to agree under k-general transmission.