Sign-changing inversions and Weierstrass partitions

This file proves Proposition 6.10 (prop:sciLambda) of the twice-marked banana paper: the number of sign-changing inversions of a transmission permutation is the size of the Weierstrass partition at its second marked point.

theorem Bananas.transmission_neg_poleOrder_nonpos {G : CFGraph} (u v : G.V) (hG : _root_.graphConnected G) (D : CFDiv G) (tau : ℤ → ℤ) (hTau : IsTransmissionPermutation (mark G u v) D tau) (i : ℕ) : tau (-poleOrder G v D i) ≤ 0

At every pole order the transmission permutation takes a nonpositive value. The relevant position is -s_i, correcting the missing minus sign in the prose proof of Proposition 6.10.

theorem Bananas.exists_eq_neg_poleOrder_of_transmission_nonpos {G : CFGraph} (u v : G.V) (hG : _root_.graphConnected G) (D : CFDiv G) (tau : ℤ → ℤ) (hTau : IsTransmissionPermutation (mark G u v) D tau) {b : ℤ} (hb : tau b ≤ 0) : ∃ (i : ℕ), b = -poleOrder G v D i

Every nonpositive transmission value occurs at exactly one negated pole order.

theorem Bananas.northwest_ncard_neg_poleOrder_eq_weierstrassPart {G : CFGraph} (u v : G.V) (hG : _root_.graphConnected G) (D : CFDiv G) (tau : ℤ → ℤ) (hTau : IsTransmissionPermutation (mark G u v) D tau) (i : ℕ) : (northwestSet tau 1 (-poleOrder G v D i)).ncard = weierstrassPart G v D i

The northwest fiber at the negated ith pole has cardinality the ith Weierstrass part.

def Bananas.sciRow (tau : ℤ → ℤ) (b : ℤ) : Set (ℤ × ℤ)

The sign-changing inversions in the row with second coordinate b.

Equations

• Bananas.sciRow tau b = (fun (a : ℤ) => (a, b)) '' northwestSet tau 1 b

theorem Bananas.sciRow_ncard (tau : ℤ → ℤ) (b : ℤ) : (sciRow tau b).ncard = (northwestSet tau 1 b).ncard

theorem Bananas.sci_eq_weierstrassSize {G : CFGraph} (u v : G.V) (hG : _root_.graphConnected G) (D : CFDiv G) (tau : ℤ → ℤ) (hTau : IsTransmissionPermutation (mark G u v) D tau) : sci tau = weierstrassSize hG v D