Unequal periods force recurrence on an opposite-side genus-one wedge

This is the period-comparison calculation in the distinct-loop branch of Theorem 4.13. The generic residue contradiction is kept in NonrecurrenceWitness; this file supplies the wedge rank witnesses.

theorem Bananas.not_nonRecurrent_of_left_torsionWitness_lt_wedge_period (G H : CFGraph) (x : G.V) (y : H.V) (u : G.V) (v : H.V) (a k : ℕ) (hHConnected : _root_.graphConnected H) (hHGenus : H.genus = 1) (ha : TorsionWitness (mark G u x) a) (haOne : 1 < a) (haK : a < k) : ¬NonRecurrent (mark (Utilities.vertexWedge G H x y) (Sum.inl u) (Utilities.wedgeRightVertex G H x y v)) k

A nontrivial torsion witness on the left factor which is strictly smaller than the wedge period produces two distinct effective twists of the right marked vertex. Hence the wedge difference is recurrent.

theorem Bananas.left_torsionOrder_eq_of_nonRecurrent_of_le (G H : CFGraph) (x : G.V) (y : H.V) (u : G.V) (v : H.V) (a b k : ℕ) (hHConnected : _root_.graphConnected H) (hHGenus : H.genus = 1) (hA : IsTorsionOrder (mark G u x) a) (hB : IsTorsionOrder (mark H y v) b) (hW : IsTorsionOrder (mark (Utilities.vertexWedge G H x y) (Sum.inl u) (Utilities.wedgeRightVertex G H x y v)) k) (hNonrec : NonRecurrent (mark (Utilities.vertexWedge G H x y) (Sum.inl u) (Utilities.wedgeRightVertex G H x y v)) k) (haOne : 1 < a) (hAB : a ≤ b) : a = b

In the distinct-factor situation, once the left period is chosen no larger than the right period, nonrecurrence forces the two exact periods to coincide. The hypotheses 1 < a and genus one on the right are exactly the nondegenerate cycle conditions used by the paper's period comparison.