Restricting torsion from an opposite-side vertex wedge

The Jacobian of a vertex wedge is a product. This file records the torsion-witness direction needed in the genus-two wedge branch: a torsion witness for an opposite-side pair restricts to witnesses for the two factor pairs. The proof uses the exact winnability convolution, avoiding a separate Jacobian-product construction.

theorem Bananas.torsionWitness_factors_of_vertexWedge_opposite (G H : CFGraph) (x : G.V) (y : H.V) (u : G.V) (v : H.V) (k : ℕ) (hW : TorsionWitness (mark (Utilities.vertexWedge G H x y) (Sum.inl u) (Utilities.wedgeRightVertex G H x y v)) k) : TorsionWitness (mark G u x) k ∧ TorsionWitness (mark H y v) k

A torsion witness for an opposite-side marked vertex wedge restricts to torsion witnesses of the same period on the two factor markings.

theorem Bananas.exists_factor_torsionOrders_of_vertexWedge_opposite (G H : CFGraph) (x : G.V) (y : H.V) (u : G.V) (v : H.V) (k : ℕ) (hW : TorsionWitness (mark (Utilities.vertexWedge G H x y) (Sum.inl u) (Utilities.wedgeRightVertex G H x y v)) k) : ∃ (a : ℕ) (b : ℕ), IsTorsionOrder (mark G u x) a ∧ IsTorsionOrder (mark H y v) b

A positive torsion witness on an opposite-side wedge supplies exact torsion orders for both factor markings.

theorem Bananas.IsTorsionOrder.eq_of_same_marked_graph {M : TwiceMarked} {a b : ℕ} (ha : IsTorsionOrder M a) (hb : IsTorsionOrder M b) : a = b

Exact torsion orders are unique. This small API lemma is useful when a normal form provides two independent descriptions of the same marked Jacobian class.

theorem Bananas.isTorsionOrder_vertexWedge_opposite_lcm (G H : CFGraph) (x : G.V) (y : H.V) (u : G.V) (v : H.V) (a b : ℕ) (hG : IsTorsionOrder (mark G u x) a) (hH : IsTorsionOrder (mark H y v) b) : IsTorsionOrder (mark (Utilities.vertexWedge G H x y) (Sum.inl u) (Utilities.wedgeRightVertex G H x y v)) (a.lcm b)

The exact order of an opposite-side marked wedge is the least common multiple of the exact orders on its two factors. Together with torsionWitness_factors_of_vertexWedge_opposite, this is the precise Jacobian-product statement needed for the distinct-loop branch of Theorem 4.13.

theorem Bananas.exists_factor_torsionOrders_lcm_eq_of_vertexWedge_opposite_kGeneral (G H : CFGraph) (x : G.V) (y : H.V) (u : G.V) (v : H.V) (k : ℕ) (hConn : _root_.graphConnected (Utilities.vertexWedge G H x y)) (hPos : 0 < (Utilities.vertexWedge G H x y).genus) (huv : Sum.inl u ≠ Utilities.wedgeRightVertex G H x y v) (hK : KGeneralTransmission (mark (Utilities.vertexWedge G H x y) (Sum.inl u) (Utilities.wedgeRightVertex G H x y v)) k) : ∃ (a : ℕ) (b : ℕ), IsTorsionOrder (mark G u x) a ∧ IsTorsionOrder (mark H y v) b ∧ k = a.lcm b

For a general-transmission opposite-side wedge, the asserted period is the least common multiple of the exact factor orders. Unlike the usual cycle presentation argument, this extracts the factor orders directly from the wedge torsion witness.