Genus-two transmission inversions

This file begins the formalization of paper Lemma lem:invtau (Lemma 4.10). The first ingredient is the paper's pointwise construction: a rank-zero, degree-one twist determines a unique inversion crossing the corresponding row and column of the transmission permutation.

def Bananas.kInversionsBySecond (k : ℕ) (τ : ℤ → ℤ) : Set (ℤ × ℤ)

The same k-inversion classes, represented by putting the second coordinate in the fundamental period. The proof of Lemma 4.10 sums the inversion rows in precisely this normalization. We retain the original kInversions definition (which normalizes the first coordinate) for the public K-general-transmission contract.

Equations

• Bananas.kInversionsBySecond k τ = {p : ℤ × ℤ | p.1 < p.2 ∧ τ p.1 > τ p.2 ∧ 0 ≤ p.2 ∧ p.2 < ↑k}

def Bananas.effectiveDegreeOneTwistResidues (M : TwiceMarked) (D : CFDiv M.graph) (k : ℕ) : Set (Fin k)

The effective degree-one members of the finite torsion orbit of D. This is the concrete Fin k model for the paper's set of effective classes in T_D^1.

Equations

• Bananas.effectiveDegreeOneTwistResidues M D k = {b : Fin k | 0 ≤ rank M.graph (Bananas.degreeTwistInt M D 1 ↑↑b)}

@[simp]

theorem Bananas.mem_effectiveDegreeOneTwistResidues_iff (M : TwiceMarked) (D : CFDiv M.graph) (k : ℕ) (b : Fin k) : b ∈ effectiveDegreeOneTwistResidues M D k ↔ 0 ≤ rank M.graph (degreeTwistInt M D 1 ↑↑b)

theorem Bananas.Set.ncard_le_two_of_zero_or_eq {α : Type u_1} (S : Set α) (z : α) (hPair : ∀ (x y : α), x ∈ S → y ∈ S → x = z ∨ y = z ∨ x = y) : S.ncard ≤ 2

A finite set whose only possible collision away from a designated base point is equality has cardinality at most two.

def Bananas.residueShift (k : ℕ) (b c : Fin k) : Fin k

Translate a finite torsion index by a fixed index, retaining its integer Euclidean representative in the half-open fundamental period.

Equations

• Bananas.residueShift k b c = b - c

@[simp]

theorem Bananas.residueShift_val (k : ℕ) (b c : Fin k) : ↑↑(residueShift k b c) = (↑↑b - ↑↑c) % ↑k

theorem Bananas.residueShift_injective (k : ℕ) (c : Fin k) : Function.Injective fun (b : Fin k) => residueShift k b c

Translating finite residue indices is injective.

theorem Bananas.deg_effectiveDegreeOneTwistResidue (M : TwiceMarked) (D : CFDiv M.graph) (k : ℕ) (b : Fin k) : CFDiv.degree (degreeTwistInt M D 1 ↑↑b) = 1

Every member of the finite twist family has degree one.

theorem Bananas.degreeTwistInt_rebase_linearEquiv {M : TwiceMarked} (D : CFDiv M.graph) (b c : ℤ) (w : M.graph.V) (hc : linearEquiv M.graph (degreeTwistInt M D 1 c) (oneChip w)) : linearEquiv M.graph (degreeTwistInt M D 1 b) (oneChip w + (b - c) • (oneChip M.u - oneChip M.v))

Rebase a degree-one twist family at any one of its representatives.

theorem Bananas.degreeTwistInt_rebase_mod_period_linearEquiv {M : TwiceMarked} {k : ℕ} (hk : TorsionWitness M k) (D : CFDiv M.graph) (b c : ℤ) (w : M.graph.V) (hc : linearEquiv M.graph (degreeTwistInt M D 1 c) (oneChip w)) : linearEquiv M.graph (degreeTwistInt M D 1 b) (oneChip w + ((b - c) % ↑k) • (oneChip M.u - oneChip M.v))

Rebased twists may be reduced to their Euclidean residue at a torsion period.

theorem Bananas.rank_nonneg_rebased_residue_of_effectiveDegreeOneTwist {M : TwiceMarked} {k : ℕ} (hk : TorsionWitness M k) (D : CFDiv M.graph) (b c : Fin k) (w : M.graph.V) (hc : linearEquiv M.graph (degreeTwistInt M D 1 ↑↑c) (oneChip w)) (hb : b ∈ effectiveDegreeOneTwistResidues M D k) : 0 ≤ rank M.graph (oneChip w + ((↑↑b - ↑↑c) % ↑k) • (oneChip M.u - oneChip M.v))

Effectiveness of a finite degree-one twist transfers to the corresponding residue twist at any chosen vertex representative.

theorem Bananas.rank_eq_zero_of_deg_one_rank_nonneg_banana_two (B : Banana 2) (X : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (hDegree : CFDiv.degree X = 1) (hRank : 0 ≤ rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) X) : rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) X = 0

On a genus-two banana, every degree-one divisor of nonnegative rank has rank exactly zero. This lets the effective degree-one twists in Lemma 4.10 feed directly into the unique-crossing construction below.

theorem Bananas.rank_effectiveDegreeOneTwistResidue_eq_zero (B : Banana 2) (u v : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (k : ℕ) (b : Fin k) (hb : b ∈ effectiveDegreeOneTwistResidues (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) u v) D k) : rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (degreeTwistInt (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) u v) D 1 ↑↑b) = 0

Effective degree-one torsion residues on a theta graph have rank zero.

theorem Bananas.effectiveDegreeOneTwistResidues_ncard_le_two_of_nonRecurrent (B : Banana 2) (u v : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (k : ℕ) (hk : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) u v) k) (hNonrec : NonRecurrent (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) u v) k) : (effectiveDegreeOneTwistResidues (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) u v) D k).ncard ≤ 2

Nonrecurrence bounds the number of effective degree-one classes in a finite exact torsion orbit by two. This is the main term estimate in the genus-two inversion formula.

theorem Bananas.degree_one_rank_zero_twist_unique_crossing_inversion (M : TwiceMarked) (D : CFDiv M.graph) (hconn : _root_.graphConnected M.graph) (hGenus : M.graph.genus = 2) (tau : ℤ → ℤ) (hTau : IsTransmissionPermutation M D tau) (a b : ℤ) (hDegree : CFDiv.degree (D + a • oneChip M.u - b • oneChip M.v) = 1) (hRank : rank M.graph (D + a • oneChip M.u - b • oneChip M.v) = 0) : ∃! p : ℤ × ℤ, p.1 < b ∧ b ≤ p.2 ∧ tau p.1 > a ∧ tau p.2 ≤ a

A rank-zero degree-one twist on a connected genus-two graph determines a unique inversion crossing its transmission corner. More explicitly, if X = D + a*u - b*v, there is a unique pair (m,n) with m < b ≤ n and τ(m) > a ≥ τ(n).

This is the pointwise construction used at the start of the proof of paper Lemma lem:invtau (Lemma 4.10). The two singleton sets are respectively the northwest and southeast quadrants at (a+1,b); Riemann--Roch makes both cardinalities equal to one.

theorem Bananas.degree_one_rank_zero_twist_exists_inversion (M : TwiceMarked) (D : CFDiv M.graph) (hconn : _root_.graphConnected M.graph) (hGenus : M.graph.genus = 2) (tau : ℤ → ℤ) (hTau : IsTransmissionPermutation M D tau) (a b : ℤ) (hDegree : CFDiv.degree (D + a • oneChip M.u - b • oneChip M.v) = 1) (hRank : rank M.graph (D + a • oneChip M.u - b • oneChip M.v) = 0) : ∃ (m : ℤ) (n : ℤ), (m, n) ∈ invSet tau ∧ m < b ∧ b ≤ n ∧ tau m > a ∧ tau n ≤ a

The pair produced by degree_one_rank_zero_twist_unique_crossing_inversion is, in particular, an ordinary inversion of the transmission permutation.

theorem Bananas.crossing_inversion_conditions_add_period {k : ℕ} {tau : ℤ → ℤ} (hAffine : IsKAffine k tau) {a b m n : ℤ} (hCross : m < b ∧ b ≤ n ∧ tau m > a ∧ tau n ≤ a) : m + ↑k < b + ↑k ∧ b + ↑k ≤ n + ↑k ∧ tau (m + ↑k) > a + ↑k ∧ tau (n + ↑k) ≤ a + ↑k

Crossing-inversion inequalities are equivariant under an affine period. Together with uniqueness of the crossing inversion, this is the descent of the pointwise twist construction to period-k inversion classes.

theorem Bananas.inversion_normalize_first_coordinate {k : ℕ} {tau : ℤ → ℤ} (hk : 0 < k) (hAffine : IsKAffine k tau) {m n : ℤ} (hInv : (m, n) ∈ invSet tau) : (m % ↑k, n - m / ↑k * ↑k) ∈ kInversions k tau

Every ordinary inversion of a positive-period affine permutation has its unique simultaneous period translate whose first coordinate lies in the fundamental range used by kInversions.

theorem Bananas.inversion_normalize_second_coordinate {k : ℕ} {tau : ℤ → ℤ} (hk : 0 < k) (hAffine : IsKAffine k tau) {m n : ℤ} (hInv : (m, n) ∈ invSet tau) : (m - n / ↑k * ↑k, n % ↑k) ∈ kInversionsBySecond k tau

Every ordinary inversion of a positive-period affine permutation also has its unique simultaneous period translate whose second coordinate lies in the fundamental range. This is the normalization used in the double-sum proof of Lemma 4.10.