Period separation for the corrected cross-one-off block, without a length

hypothesis

crossOneOff_cutoff_le_torsionOrder (Bananas/CrossOneOffPeriodSeparation.lean) proves crossOneOffCutoff g (B.length beta) ≤ k for the near-opposite marking (v_{α,1}, v_{β,n_β-1}) only under the extra hypothesis hBetaLong : g + 1 ≤ B.length beta. This file removes that hypothesis: the sharp bound holds for every torsion witness whenever the two strand lengths are not both equal to two.

The argument (Bananas/FORMALIZATION_NOTES.md, "the short-strand period separation is provable — closed-form torsion order") extracts from the slope framework of Bananas/BananaTorsionSlopes.lean the exact identity m = p + r + Σ_γ q_γ where p := d/a, r := d/b (d a common multiple of the two marked lengths) and each q_γ a common-multiple share of |rise| over the other strands, then a ray/primitivity argument on the two integers D := lcm(a,b) - a/gcd(a,b) - b/gcd(a,b) and E := L + Σ_γ L/n_γ (L := lcm of the other lengths).

Generic finite-sum helpers

Pure arithmetic lemmas

The Banana-specific extraction and assembly

theorem Bananas.crossOneOff_cutoff_le_torsionWitness_of_not_both_two {g : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) : 3 ≤ g → ∀ (hab : alpha ≠ beta) (hAlpha : 1 < B.length alpha) (hBeta : 1 < B.length beta) (hNotBoth : ¬(B.length alpha = 2 ∧ B.length beta = 2)) (m : ℕ) (hm : TorsionWitness (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) m), crossOneOffCutoff g (B.length beta) ≤ m

Core lemma: every torsion witness of the near-opposite cross-one-off marking satisfies the closed-form cutoff bound, without any hypothesis relating the two marked strand lengths beyond the two lengths not both being 2.

theorem Bananas.crossOneOff_cutoff_le_torsionOrder_of_not_both_two {g k : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (hg : 3 ≤ g) (hab : alpha ≠ beta) (hAlpha : 1 < B.length alpha) (hBeta : 1 < B.length beta) (hNotBoth : ¬(B.length alpha = 2 ∧ B.length beta = 2)) (hTO : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) k) : crossOneOffCutoff g (B.length beta) ≤ k

Corollary: the closed-form period-separation bound for the exact torsion order, replacing the long-second-strand hypothesis hBetaLong of crossOneOff_cutoff_le_torsionOrder by the weaker hNotBoth.