Period extraction from a rigid genus-two wedge

This is the converse-period component of the distinct-factor branch of Theorem 4.13. Once factor torsion orders have been identified, general transmission on a bridgeless rigid wedge forces the smaller nontrivial order to equal the other one.

theorem Bananas.factor_torsionOrders_eq_of_vertexWedge_opposite_kGeneral {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) (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))) (haOne : 1 < a) (hAB : a ≤ b) (hK : KGeneralTransmission (mark (Utilities.vertexWedge G H x y) (Sum.inl u) (Utilities.wedgeRightVertex G H x y v)) k) : a = b

In the ordered distinct-factor wedge branch, k-general transmission forces the two nontrivial factor torsion orders to agree. The factor exact orders are deliberately explicit: constructing them from a concrete cycle presentation is a separate, purely topological part of the global classification.

theorem Bananas.pointedGenusOneRigid_vertexWedge_opposite_kGeneral_iff_orders_eq {G H : CFGraph} (x : G.V) (y : H.V) (u : G.V) (v : H.V) (a b : ℕ) (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))) (haOne : 1 < a) (hAB : a ≤ b) : KGeneralTransmission (mark (Utilities.vertexWedge G H x y) (Sum.inl u) (Utilities.wedgeRightVertex G H x y v)) (a.lcm b) ↔ a = b

Exact distinct-factor branch of Theorem 4.13 in the intrinsic pointed-rigid interface. At the (necessarily lcm) wedge torsion order, general transmission is equivalent to equality of the two ordered, nontrivial factor orders.