Torsion order two plus submodularity gives 2-general transmission

Paper source: lem-TO2GenTrans (Lemma 4.3). This is the (only) partial converse to lem:kgtImpliesTorsionOrder (Lemma 4.2, TorsionOrderExact.lean): at k = 2 exactly, torsion order plus all-divisor submodularity is already enough to force 2-general transmission, without any further geometric input.

The proof follows the published argument. The existence/periodicity half of KGeneralTransmission is already available from exists_affine_transmission_of_allSubmodular. What remains is the 2-inversion count bound kInversionCount 2 τ ≤ genus, which the paper derives from the Riemann-Roch inequality eq-RRTauBounds: b - deg D ≤ τ_D(b) ≤ 2g + b - deg D. We prove this bound directly (as transmissionPermutation_ge / transmissionPermutation_le, valid for any transmission permutation of any connected twice-marked graph, no submodularity needed), then combine the two consecutive instances at b = 0 and b = 1 with the periodicity τ(n + 2) = τ(n) + 2 to bound the 2-inversion count.

The Riemann-Roch bound on a transmission permutation

theorem Bananas.transmissionPermutation_ge {M : TwiceMarked} {D : CFDiv M.graph} {τ : ℤ → ℤ} (hτ : IsTransmissionPermutation M D τ) (b : ℤ) : b - CFDiv.degree D ≤ τ b

Paper source: eq-RRTauBounds, lower half. No submodularity is needed: this is a direct consequence of the two-term rank-vanishing pattern below the degree-0 threshold.

theorem Bananas.transmissionPermutation_le {M : TwiceMarked} {D : CFDiv M.graph} {τ : ℤ → ℤ} (hconn : _root_.graphConnected M.graph) (hτ : IsTransmissionPermutation M D τ) (b : ℤ) : τ b ≤ 2 * M.graph.genus + b - CFDiv.degree D

Paper source: eq-RRTauBounds, upper half. Uses rank_nonspecial_range (Riemann's part of Riemann-Roch) rather than submodularity.

The 2-inversion count bound

theorem Bananas.kInversionCount_two_le_genus {M : TwiceMarked} {D : CFDiv M.graph} {τ : ℤ → ℤ} (hconn : _root_.graphConnected M.graph) (hτ : IsTransmissionPermutation M D τ) (hAff : IsKAffine 2 τ) : kInversionCount 2 τ ≤ M.graph.genus.toNat

Paper source: proof of lem-TO2GenTrans. Any affine transmission permutation at period 2 has 2-inversion count at most the genus, regardless of submodularity: the bound only uses transmissionPermutation_ge / transmissionPermutation_le at b = 0, 1 together with the periodicity τ(n + 2) = τ(n) + 2.

Main theorem

theorem Bananas.torsionOrder_two_allSubmodular_isKGeneral {M : TwiceMarked} (hconn : _root_.graphConnected M.graph) (hTO : IsTorsionOrder M 2) (hSub : AllSubmodular M) : KGeneralTransmission M 2

Paper source: lem-TO2GenTrans (Lemma 4.3).

If (G, u, v) has torsion order exactly 2 and every divisor is submodular, then (G, u, v) has 2-general transmission. This is a genuine partial converse to lem:kgtImpliesTorsionOrder (KGeneralTransmission.isTorsionOrder in TorsionOrderExact.lean), valid only at k = 2: connectivity is the only hypothesis needed beyond the paper statement, matching every other theorem in this file's dependency chain.