General transmission on pointed rigid genus-one factors

PointedGenusOneRigid supplies exactly the degree-one rigidity needed to derive all-divisor submodularity for a distinct marking. Combined with the genus-one transmission theorem, this turns an exact torsion calculation on a cycle factor directly into KGeneralTransmission.

theorem Bananas.pointedGenusOneRigid_kGeneral_of_isTorsionOrder {G : CFGraph} (x u : G.V) (hRigid : Utilities.PointedGenusOneRigid G x) (hu : u ≠ x) {k : ℕ} (hOrder : IsTorsionOrder (mark G u x) k) : KGeneralTransmission (mark G u x) k

A distinct marking on a pointed rigid genus-one graph is k-general at its exact torsion order. This is the factor-level input needed in the opposite-side vertex-wedge branch of Theorem 4.13.

theorem Bananas.pointedGenusOneRigid_vertexWedge_opposite_kGeneral_of_isTorsionOrder {G H : CFGraph} (x : G.V) (y : H.V) (u : G.V) (v : H.V) (k : ℕ) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hu : u ≠ x) (hv : v ≠ y) (hGOrder : IsTorsionOrder (mark G u x) k) (hHOrder : IsTorsionOrder (mark H y v) k) : KGeneralTransmission (mark (Utilities.vertexWedge G H x y) (Sum.inl u) (Utilities.wedgeRightVertex G H x y v)) k

The opposite-side wedge of two pointed rigid genus-one factors is k-general as soon as the two factor markings have the same exact torsion order. This is the forward wedge clause in Theorem 4.13 with all factor-level submodularity and transmission hypotheses discharged.