Corrected high-genus banana torsion dichotomy

This is the one remaining non-Section-6 input to the corrected Corollary 6.4. The paper's exceptional family is corrected here: one of the two marked midpoint strands need only have length two; the other may have any even length.

theorem Bananas.allSubmodular_implies_nsmForBananaException {g : ℕ} (hg : 3 ≤ g) (B : Banana g) (α β : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hSub : AllSubmodular (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j))) : NSMForBananaException B (strandVertex B α i) (strandVertex B β j)

The completed corrected Theorem 3.9 gives the first reduction for Proposition 4.19: all-divisor submodularity forces one of its explicit endpoint-aware exceptional families.

theorem Bananas.corrected_banana_torsion_dichotomy {g k : ℕ} (hg : 3 ≤ g) (B : Banana g) (α β : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hTO : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j)) k) (hSub : AllSubmodular (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j))) : CorrectedMidpointException B α β i j ∧ k = 2 ∨ g ≤ k

Corrected Proposition 4.19 (prop-bananTorsion).

Outside the corrected midpoint family, every exact torsion order compatible with all-divisor submodularity is at least the genus. The proof combines the completed Theorem 3.9 classification with the endpoint and near-opposite slope bounds and the reduced-divisor midpoint lemma lem-midpointTorsion. The statement is deliberately separate from the Section 6 assembly so that no later theorem can silently use an unrecorded classification assumption.