The cross-one-off obstruction to general transmission

The exact-torsion theorem supplies the period separation that ordinary inversion counting needs. In the long-second-strand regime, the exceptional order-two branch of the corrected torsion dichotomy is impossible, so a k-general marking has g ≤ k. The corrected decreasing block then has more than genus = g inversions as soon as g ≥ 7.

theorem Bananas.crossOneOff_kGeneral_period_ge_genus {g k : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (hg : 3 ≤ g) (hab : alpha ≠ beta) (hAlpha : 1 < B.length alpha) (hBetaLong : g + 1 ≤ B.length beta) (hK : KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) k) : g ≤ k

In the long-second-strand regime, k-general transmission forces the period to be at least the genus. This is the graph-theoretic separation missing from a count based only on the forced rows of corrected Lemma 4.30.

The proof uses exactness of the k-general period and corrected Lemma 4.27. Its order-two midpoint alternative cannot occur because the second mark is the penultimate point of a strand of length at least g+1 > 2.

theorem Bananas.crossOneOff_not_kGeneral_of_seven_le_genus {g k : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (hg : 7 ≤ 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

The corrected Corollary 4.29 block directly rules out k-general transmission in genus at least seven, under the explicit long-strand range needed by the row calculation.

The threshold 7 is sharp for this particular block: it contributes choose (g-2) 2 inversions, which first exceeds the genus at g=7. No claim about the still-unproved larger count of Corollary 4.31 is used.