Rank differences in genus one

For a connected genus-one graph, Riemann--Roch makes the marked second rank difference completely local in degrees 0, 1, and 2. This is the rank-theoretic core needed to identify genus-one transmission permutations as an affine translation with at most one adjacent interchange.

theorem Bananas.kInversionCount_eq_zero_of_translation (k : ℕ) (tau : ℤ → ℤ) (c : ℤ) (hTau : ∀ (n : ℤ), tau n = n + c) : kInversionCount k tau = 0

A translated identity permutation has no affine inversion classes, at any period. This is the zero-principal-orbit case of genus-one transmission.

theorem Bananas.kInversionCount_output_translate (k : ℕ) (tau : ℤ → ℤ) (s : ℤ) : (kInversionCount k fun (n : ℤ) => tau n + s) = kInversionCount k tau

Translating all values of a permutation leaves its normalized inversion classes unchanged.

theorem Bananas.kInversionCount_output_translate_affineReflection_le_one (k : ℕ) (i s : ℤ) (hk : 2 ≤ k) : (kInversionCount k fun (n : ℤ) => (affineReflection k i hk).func n + s) ≤ 1

Hence a value-translate of one periodic affine simple reflection has at most one inversion class.

theorem Bananas.rankDelta_genusOne_of_degree_neg {G : CFGraph} {u v : G.V} {X : CFDiv G} (hDegree : CFDiv.degree X < 0) : rankDelta (mark G u v) X = 0

In negative degree, every term in the marked rank difference vanishes.

theorem Bananas.rankDelta_genusOne_of_degree_zero {G : CFGraph} {u v : G.V} {X : CFDiv G} (hDegree : CFDiv.degree X = 0) : rankDelta (mark G u v) X = rank G X + 1

The degree-zero row is exactly the principality indicator, written as rank X + 1.

theorem Bananas.rankDelta_genusOne_of_degree_one {G : CFGraph} {u v : G.V} {X : CFDiv G} (hConnected : _root_.graphConnected G) (hGenus : G.genus = 1) (hDegree : CFDiv.degree X = 1) : rankDelta (mark G u v) X = -rank G (X - oneChip u) - rank G (X - oneChip v) - 1

In degree one, only the two degree-zero residual classes can affect the marked rank difference.

theorem Bananas.rankDelta_genusOne_of_degree_two {G : CFGraph} {u v : G.V} {X : CFDiv G} (hConnected : _root_.graphConnected G) (hGenus : G.genus = 1) (hDegree : CFDiv.degree X = 2) : rankDelta (mark G u v) X = rank G (X - oneChip u - oneChip v) + 1

The degree-two row is the principality indicator of the double deletion.

theorem Bananas.rankDelta_genusOne_of_degree_gt_two {G : CFGraph} {u v : G.V} {X : CFDiv G} (hConnected : _root_.graphConnected G) (hGenus : G.genus = 1) (hDegree : 2 < CFDiv.degree X) : rankDelta (mark G u v) X = 0

Above degree two, Riemann--Roch makes the four ranks affine-linear, so their second difference is zero.

def Bananas.genusOneZeroTwist {G : CFGraph} {u v : G.V} (D : CFDiv G) (b : ℤ) : CFDiv G

The degree-zero member of the marked twist orbit at index b.

Equations

• Bananas.genusOneZeroTwist D b = D + (b - CFDiv.degree D) • oneChip u - b • oneChip v

theorem Bananas.transmission_eq_translation_of_no_principal_genusOne {G : CFGraph} {u v : G.V} (hConnected : _root_.graphConnected G) (hGenus : G.genus = 1) (D : CFDiv G) (tau : ℤ → ℤ) (hTau : IsTransmissionPermutation (mark G u v) D tau) (hNoPrincipal : ∀ (b : ℤ), ¬linearEquiv G (genusOneZeroTwist D b) 0) (b : ℤ) : tau b = b - CFDiv.degree D + 1

If a genus-one marked twist orbit has no principal degree-zero member, the transmission permutation is the corresponding translated identity.

theorem Bananas.kInversionCount_eq_zero_of_no_principal_genusOne {G : CFGraph} {u v : G.V} (hConnected : _root_.graphConnected G) (hGenus : G.genus = 1) (D : CFDiv G) (tau : ℤ → ℤ) (k : ℕ) (hTau : IsTransmissionPermutation (mark G u v) D tau) (hNoPrincipal : ∀ (b : ℤ), ¬linearEquiv G (genusOneZeroTwist D b) 0) : kInversionCount k tau = 0

Consequently, the no-principal-orbit transmission has zero inversion classes at every period.

theorem Bananas.transmission_value_of_principal_genusOneZeroTwist {G : CFGraph} {u v : G.V} (D : CFDiv G) (tau : ℤ → ℤ) (c : ℤ) (hTau : IsTransmissionPermutation (mark G u v) D tau) (hPrincipal : linearEquiv G (genusOneZeroTwist D c) 0) : tau c = c - CFDiv.degree D

A principal degree-zero twist supplies the lowered transmission row at its own index.

theorem Bananas.transmission_value_before_principal_genusOneZeroTwist {G : CFGraph} {u v : G.V} (hConnected : _root_.graphConnected G) (hGenus : G.genus = 1) (D : CFDiv G) (tau : ℤ → ℤ) (c : ℤ) (hTau : IsTransmissionPermutation (mark G u v) D tau) (hPrincipal : linearEquiv G (genusOneZeroTwist D c) 0) : tau (c - 1) = c - CFDiv.degree D + 1

The row immediately preceding a principal degree-zero twist is raised by one. This is the other half of the affine adjacent interchange.

theorem Bananas.not_principal_genusOneZeroTwist_of_not_dvd {G : CFGraph} {u v : G.V} {k : ℕ} (hOrder : IsTorsionOrder (mark G u v) k) (D : CFDiv G) (b c : ℤ) (hPrincipal : linearEquiv G (genusOneZeroTwist D c) 0) (hNotDvd : ¬k ∣ (b - c).natAbs) : ¬linearEquiv G (genusOneZeroTwist D b) 0

At an exact torsion order, a principal degree-zero twist can occur only in its own residue class.

theorem Bananas.transmission_value_of_two_nonprincipal_genusOneZeroTwists {G : CFGraph} {u v : G.V} (hConnected : _root_.graphConnected G) (hGenus : G.genus = 1) (D : CFDiv G) (tau : ℤ → ℤ) (b : ℤ) (hTau : IsTransmissionPermutation (mark G u v) D tau) (hB : ¬linearEquiv G (genusOneZeroTwist D b) 0) (hNext : ¬linearEquiv G (genusOneZeroTwist D (b + 1)) 0) : tau b = b - CFDiv.degree D + 1

Away from a principal degree-zero twist and its successor, the genus-one transmission row is the ordinary translated-identity row.