One-off general-transmission obstruction

This packages the corrected immediate inversion estimate following Lemma 4.23 with the defining inversion upper bound for KGeneralTransmission. The arithmetic hypothesis is deliberately explicit: it is exactly the condition under which the paper's one-off row block is large enough to obstruct generality.

theorem Bananas.oneOff_not_kGeneral_of_inversion_bound_gt_genus {g k : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (hg : 2 ≤ g) (hLength : 1 < B.length alpha) (hLarge : g < ((B.length alpha - 2) * (g / (B.length alpha - 1))).choose 2) : ¬KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) k

The one-off marking cannot have k-general transmission once the explicit inversion block from Lemma 4.24 is larger than the genus.