Arithmetic ranges for the cross one-off transmission block

This file isolates the meaning of "sufficiently long" in the both-off case of Section 4.4.3 of the twice-marked banana paper. If n₁ is the length of the second marked strand, the integral endpoint of the paper's rational interval

b ≤ (n₁ / (n₁ - 1)) g

is g + g / (n₁ - 1). The length assumption below is the exact uniform threshold for the corrected block. The three numerical bounds in Lemma 4.30 belong to three different congruence classes; in particular, its second bound is not asserted for every integer below the cutoff.

def Bananas.crossOneOffCutoff (g n : ℕ) : ℕ

The largest natural number in the interval b ≤ (n / (n - 1)) g, for 1 < n.

Equations

• Bananas.crossOneOffCutoff g n = g + g / (n - 1)

def Bananas.CrossOneOffLongEnough (g n₀ n₁ : ℕ) : Prop

A precise, uniform version of the paper's phrase "the first marked strand is sufficiently long relative to the genus". The minimal integral threshold needed for the corrected block is g + 1 + g / (n₁ - 1) ≤ n₀.

Equations

• Bananas.CrossOneOffLongEnough g n₀ n₁ = (g + 1 + g / (n₁ - 1) ≤ n₀)

theorem Bananas.crossOneOffCutoff_eq_mul_div {g n : ℕ} (hn : 1 < n) : crossOneOffCutoff g n = n * g / (n - 1)

The rational cutoff from the paper has the indicated natural-number form.

theorem Bananas.crossOneOffLongEnough_ranges {g n₀ n₁ b : ℕ} (hg : 1 ≤ g) (hn₁ : 1 < n₁) (hlong : CrossOneOffLongEnough g n₀ n₁) (hb : b ≤ crossOneOffCutoff g n₁) : b < n₁ * (n₀ - 1) ∧ (b % n₁ = n₁ - 1 → b ≤ n₁ * (n₀ - 1 - g) - 1) ∧ (2 ≤ b → b % n₁ ≠ 0 → b % n₁ ≠ n₁ - 1 → 2 * ↑(b / n₁) - ↑b ≤ ↑n₀ - 3 - ↑g)

The exact length hypothesis simultaneously implies all three numerical side conditions used in the corrected three residue cases of Lemma 4.30. The first conclusion is only needed at positive multiples of n₁; its strict form is the interior bound b < n₁ (n₀ - 1). The endpoint allowed by the paper's weak inequality requires a separate rank argument. The third inequality is stated over ℤ, as in the paper; natural subtraction would silently truncate its negative left-hand side.