An extended cross-one-off inversion block

When the second marked strand has length at least g+2, the corrected row formula stays in its simple positive-residue case through row g. Thus the decreasing block extends from 2,...,g-1 to 2,...,g and contributes choose (g-1) 2 inversions.

The generic counting lemma below also sharpens the period boundary in shifted_decreasing_block_inversion_lower_bound: the largest first coordinate is one less than the final block coordinate, so lo + length ≤ k is enough.

theorem Bananas.shifted_decreasing_block_inversion_lower_bound_le_period {lo length value k : ℕ} {tau : ℤ → ℤ} (hValue : length ≤ value) (hSeparate : lo + length ≤ k) (hBlock : ∀ i ≤ length, tau (↑lo + ↑i) = ↑(value - i)) (hfinite : (kInversions k tau).Finite) : (length + 1).choose 2 ≤ kInversionCount k tau

A shifted decreasing block whose final coordinate is at most k contributes all pairwise inversions to kInversions k tau. Equality at the right endpoint is valid because it can occur only as the second coordinate of one of the injected inversions.

theorem Bananas.transmission_crossOneOff_extended_simple_block {g : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (tau : ℤ → ℤ) (hg : 3 ≤ g) (hab : alpha ≠ beta) (hAlpha : 1 < B.length alpha) (hBetaVeryLong : g + 2 ≤ B.length beta) (hLong : CrossOneOffLongEnough g (B.length alpha) (B.length beta)) (hTau : IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) (g • oneChip (rightEndpoint B)) tau) (i : ℕ) : i ≤ g - 2 → tau ↑(2 + i) = ↑(g - i)

If the second strand has length at least g+2, corrected Lemma 4.30 forces the extended decreasing block tau(2+i)=g-i through i=g-2.

theorem Bananas.crossOneOff_extended_simple_inversion_lower_bound {g k : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (tau : ℤ → ℤ) (hg : 3 ≤ g) (hab : alpha ≠ beta) (hAlpha : 1 < B.length alpha) (hBetaVeryLong : g + 2 ≤ B.length beta) (hLong : CrossOneOffLongEnough g (B.length alpha) (B.length beta)) (hTau : IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) (g • oneChip (rightEndpoint B)) tau) (hSeparate : g ≤ k) (hfinite : (kInversions k tau).Finite) : (g - 1).choose 2 ≤ kInversionCount k tau

The extended simple block contributes choose (g-1) 2 normalized inversions as soon as g ≤ k.

theorem Bananas.crossOneOff_not_kGeneral_of_five_le_genus {g k : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (hg : 5 ≤ g) (hab : alpha ≠ beta) (hAlpha : 1 < B.length alpha) (hBetaVeryLong : g + 2 ≤ B.length beta) (hLong : CrossOneOffLongEnough g (B.length alpha) (B.length beta)) : ¬KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) k

For a second strand strictly longer than g+1, the corrected inversion block rules out k-general transmission already in genus five.