The corrected cross-one-off transmission block

This file assembles the three residue-specific calculations of corrected Lemma 4.30 over the full interval guaranteed by CrossOneOffLongEnough.

def Bananas.crossOneOffRow (g n b : ℕ) : ℕ

The corrected value forced in row b of the both-off transmission permutation.

Equations

• Bananas.crossOneOffRow g n b = if b % n = 0 then b / n + 1 else if b % n = n - 1 then g + b / n + 1 else g + 2 * (b / n) + 2 - b

theorem Bananas.crossOneOff_sub_div_le_genus {g n b : ℕ} (hn : 1 < n) (hb : b ≤ crossOneOffCutoff g n) : b - b / n ≤ g

Every integer in the corrected cutoff interval is at distance at most g from its quotient by the second marked-strand length.

theorem Bananas.transmission_crossOneOff_block {g : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (b : ℕ) (tau : ℤ → ℤ) (hg : 2 ≤ g) (hab : alpha ≠ beta) (hAlpha : 1 < B.length alpha) (hBeta : 1 < B.length beta) (hLong : CrossOneOffLongEnough g (B.length alpha) (B.length beta)) (hbLo : 2 ≤ b) (hbHi : b ≤ crossOneOffCutoff g (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) : tau ↑b = ↑(crossOneOffRow g (B.length beta) b)

Corrected Lemma 4.30, uniformly over its valid block.

The printed lemma has incompatible residue conventions and includes the false boundary N = 2, b = 1. Here the block starts at b = 2, uses positive remainders, and the positive-residue row has the corrected final +2.