Corrected both-off inversion lower bound

This is the graph-level assembly of the finite row injection and its exact arithmetic count. It is Corollary 4.31 with the corrected row block and its explicit period-separation hypothesis.

theorem Bananas.crossOneOff_corrected_inversion_lower_bound {g k : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (tau : ℤ → ℤ) (hg : 2 ≤ g) (hab : alpha ≠ beta) (hAlpha : 1 < B.length alpha) (hBeta : 1 < B.length beta) (hLong : CrossOneOffLongEnough g (B.length alpha) (B.length beta)) (hTau : IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) (g • oneChip (rightEndpoint B)) tau) (hSeparate : crossOneOffCutoff g (B.length beta) ≤ k) (hfinite : (kInversions k tau).Finite) : correctedCrossOneOffForcedCount g (B.length beta) ≤ kInversionCount k tau

Verified form of Corollary 4.31, conditional on the required period separation.

correctedCrossOneOffForcedCount treats a second strand of length two separately, using choose g 2 in that case and choose (g - 1) 2 + g / (n - 1) otherwise.

theorem Bananas.crossOneOff_corrected_inversion_lower_bound_of_not_both_two {g k : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (tau : ℤ → ℤ) (hg : 3 ≤ g) (hab : alpha ≠ beta) (hAlpha : 1 < B.length alpha) (hBeta : 1 < B.length beta) (hLong : CrossOneOffLongEnough g (B.length alpha) (B.length beta)) (hTau : IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) (g • oneChip (rightEndpoint B)) tau) (hTO : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) k) (hfinite : (kInversions k tau).Finite) : correctedCrossOneOffForcedCount g (B.length beta) ≤ kInversionCount k tau

Unconditional form of corrected Corollary 4.31: the period-separation hypothesis hSeparate is now supplied internally from the exact torsion order via crossOneOff_cutoff_le_torsionOrder_of_not_both_two (Bananas/CrossOneOffShortStrandPeriod.lean), since CrossOneOffLongEnough already forces B.length alpha ≥ g + 1 ≥ 4 > 2, so the two marked strand lengths can never both be 2.