The first transmission row for a same-strand one-off marking

This begins the formalization of Lemmas 4.23--4.25 for the marking consisting of the left endpoint and the penultimate point of one strand. The endpoint reflection firing rewrites subtraction of the penultimate chip into banana normal form. At the divisor g • rightEndpoint, the resulting four ranks give rankDelta = 1, hence the base transmission row tau 0 = 0.

theorem Bananas.isSemibreak_zero {g : ℕ} (B : Banana g) : IsSemibreak B 0

The zero divisor is a semibreak divisor.

theorem Bananas.oneOff_sub_penultimate_linearEquiv_normalForm {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (c : ℕ) (hLength : 1 < B.length alpha) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (↑c • oneChip (rightEndpoint B) - oneChip (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) (bananaNormalForm B (-1) (↑c - 1) (oneChip (strandVertex B alpha ⟨1, ⋯⟩)))

Endpoint reflection, rewritten in the form used after subtracting the penultimate mark from a right-endpoint multiple: cR-v_(alpha,n-1) ~ -L+(c-1)R+v_(alpha,1).

theorem Bananas.oneOff_sub_both_marks_linearEquiv_normalForm {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (c : ℕ) (hLength : 1 < B.length alpha) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (↑c • oneChip (rightEndpoint B) - oneChip (leftEndpoint B) - oneChip (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) (bananaNormalForm B (-2) (↑c - 1) (oneChip (strandVertex B alpha ⟨1, ⋯⟩)))

The corresponding reflection firing after also subtracting the left mark.

theorem Bananas.rankDelta_oneOff_rightEndpoint_nsmul_eq_one {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (c : ℕ) (hc : 0 < c) (hcg : c ≤ g) (hLength : 1 < B.length alpha) : rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) (c • oneChip (rightEndpoint B)) = 1

The rank-difference calculation behind the base row of paper Lemma 4.23. It is stated for every positive right-endpoint coefficient up to the genus; the paper application is c=g.

theorem Bananas.transmission_oneOff_zero {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (tau : ℤ → ℤ) (hg : 0 < g) (hLength : 1 < B.length alpha) (hTau : IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) (g • oneChip (rightEndpoint B)) tau) : tau 0 = 0

The first concrete transmission row of Lemma 4.23: for D=g·rightEndpoint, the same-strand one-off permutation satisfies tau(0)=0.