General transmission in genus one

The periodic assembly of the three row formulas in GenusOneRankDelta: an exact principal residue gives a translated affine simple reflection, while no principal residue gives a translation. The resulting inversion bounds are already checked in that module, so this file is composition and case analysis.

The shape of the argument, for a fixed divisor D:

• submodularity supplies a transmission permutation τ, affine at the torsion witness (exists_affineTransmissionPermutation_of_submodular);
• if no degree-zero member of the marked twist orbit is principal, τ is a translation and has no inversion classes at all;
• otherwise fix a principal index c. At an exact torsion order the principal indices are exactly c mod k, so τ lowers the row at c, raises the row at c - 1, and is the ordinary translated identity everywhere else. That is precisely affineReflection k (c-1) translated by 1 - deg D, which has at most one inversion class.

The k = 1 case is separated out because affineReflection needs 2 ≤ k. There every index is principal, so τ is again a translation.

theorem Bananas.kGeneralTransmission_genusOne_of_torsionOrder_and_allSubmodular {M : TwiceMarked} {k : ℕ} (hConnected : _root_.graphConnected M.graph) (hGenus : M.graph.genus = 1) (hOrder : IsTorsionOrder M k) (hSub : AllSubmodular M) : KGeneralTransmission M k

A connected genus-one twice-marked graph with exact torsion order and all divisors submodular has general transmission at that order.