Corrected long-strand cross-one-off obstruction

The corrected Corollary 4.31 count, together with the strict period separation, rules out k-general transmission in genus at least five as soon as the second marked strand has length at least g+1. This includes the boundary length g+1 omitted by the earlier extended-simple-block argument.

theorem Bananas.choose_genus_sub_one_two_gt_genus {g : ℕ} (hg : 5 ≤ g) : g < (g - 1).choose 2

The genus-five threshold is the first one at which the universal choose (g-1) 2 portion of the corrected count exceeds the genus.

theorem Bananas.genus_lt_correctedCrossOneOffForcedCount_of_second_long {g n : ℕ} (hg : 5 ≤ g) (hn : g + 1 ≤ n) : g < correctedCrossOneOffForcedCount g n

In the long-second-strand regime, the corrected forced count is already strictly larger than the genus for g ≥ 5.

theorem Bananas.crossOneOff_not_kGeneral_of_five_le_genus_second_long {g k : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (hg : 5 ≤ g) (hab : alpha ≠ beta) (hAlpha : 1 < B.length alpha) (hBetaLong : g + 1 ≤ 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

Corrected long-strand consequence of Corollary 4.31.

For distinct cross-one-off marks, a second strand of length at least g+1 and the corrected long-first-strand range rule out k-general transmission in every genus g ≥ 5. The threshold is sharp for this count: at g=4 and length beta = g+1, its numerical lower bound equals g.

theorem Bananas.correctedCrossOneOffForcedCount_genus_four_boundary : correctedCrossOneOffForcedCount 4 5 = 4

At the first excluded genus and the boundary strand length, the corrected numerical lower bound is exactly the KGT upper bound.

theorem Bananas.crossOneOff_not_kGeneral_boundary_second_length {g k : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (hg : 5 ≤ g) (hab : alpha ≠ beta) (hBeta : B.length beta = g + 1) (hAlphaLong : g + 2 ≤ B.length alpha) : ¬KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) k

Boundary-length specialization: when length beta = g+1, the exact long-range threshold is length alpha ≥ g+2.

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

Strictly-long specialization: when length beta ≥ g+2, the exact long-range threshold drops to length alpha ≥ g+1.