Exact torsion order from k-general transmission

Paper source: lem:kgtImpliesTorsionOrder (Lemma 4.2). A twice-marked graph with k-general transmission has k equal to its torsion order, not merely divisible by it (TorsionWitness M k, which is already hK.1, only records divisibility).

The proof follows the published argument: using the transmission permutation τ of the zero divisor, τ 0 = 0 (from r(0) = 0 and two negative-degree rank vanishings), and Riemann-Roch identifies a set A of exactly genus many negative integers a with τ a > 0, each giving a distinct ordinary inversion (a, 0). Since k-general transmission bounds the number of k-inversions by the genus, these genus-many inversions already exhaust Inv_k(τ); periodicity at any further torsion witness n then produces a new inversion (a + n, n) whose normalization forces k ∣ n.

theorem Bananas.IsTransmissionPermutation.isKAffine_of_torsionWitness {M : TwiceMarked} {D : CFDiv M.graph} {τ : ℤ → ℤ} (hτ : IsTransmissionPermutation M D τ) {m : ℕ} (hm : TorsionWitness M m) : IsKAffine m τ

Any transmission permutation of D is periodic (IsKAffine) at every torsion witness of M, not only a distinguished one. This is the periodicity half of exists_affineTransmissionPermutation_of_submodular, extracted so that it applies to a τ obtained by other means (here: the package supplied by KGeneralTransmission), without redoing the Submodular-based construction of τ.

theorem Bananas.KGeneralTransmission.isTorsionOrder {M : TwiceMarked} {k : ℕ} (hK : KGeneralTransmission M k) (_huv : M.u ≠ M.v) (hconn : _root_.graphConnected M.graph) (hg : 0 < M.graph.genus) : IsTorsionOrder M k

Paper source: lem:kgtImpliesTorsionOrder (Lemma 4.2).

k-general transmission forces k to be the exact torsion order.

Two hypotheses beyond KGeneralTransmission are needed, and both are genuine (not merely convenient) restrictions:

• huv : M.u ≠ M.v. At the diagonal marking u = v, every positive k is a TorsionWitness (TransmissionAPI.torsionWitness_diagonal), so minimality can fail without distinctness.
• hg : 0 < genus M.graph. At genus 0, Riemann-Roch forces rank D = max (deg D) (-1) for every divisor D (since deg (canonicalDivisor - D) < 0 whenever deg D ≥ 0), which makes every transmission permutation a pure shift with no inversions at all. In that case KGeneralTransmission M k holds simultaneously for every positive k (the inversion bound ≤ 0 and the periodicity clause are both vacuous, and the torsion condition is automatic since the Jacobian is trivial), so k is never pinned down to the torsion order 1. The paper implicitly works with graphs of nontrivial genus throughout this section; this hypothesis makes that explicit.

hconn : graphConnected M.graph is also required, matching the connectivity hypothesis already threaded through exists_affine_transmission_of_allSubmodular and the Riemann-Roch API.

theorem Bananas.banana_kGeneral_isTorsionOrder {g k : ℕ} (B : Banana g) (u v : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V) (huv : u ≠ v) (hg : 0 < (Utilities.Certificate.SubdivisionGraph.Spec.graph B).genus) (hK : KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) u v) k) : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) u v) k

TeX label: lem:kgtImpliesTorsionOrder (Lemma 4.2).

k-general transmission forces k to be the exact torsion order of (G, u, v), not merely a period that annihilates u - v (KGeneralTransmission.to_torsionWitness already gives that weaker fact for free). The full mechanized argument is KGeneralTransmission.isTorsionOrder above; this is a thin restatement at the mark API used by the rest of the library.

Two hypotheses beyond the paper statement are required — see the docstring of KGeneralTransmission.isTorsionOrder for why both are genuine gaps in a literal reading of the lemma (not artificial strengthenings): hconn (connectivity, needed for the Riemann-Roch input used throughout this section) and hg (positive genus, since at genus 0 every positive k satisfies KGeneralTransmission simultaneously, so k is never pinned to the torsion order 1 there). huv matches the paper's own distinctness convention (FORMALIZATION_NOTES.md, "Distinctness of the two marks"); the diagonal marking u = v has a TorsionWitness at every period (torsionWitness_diagonal), so minimality can fail without it.