The length-two part of the corrected cross-one-off finite count

For strand length two, every unordered pair of indices in Fin (g - 1) selects a distinct inversion: its smaller index selects an odd row and its larger index selects a later even row.

noncomputable def Bananas.crossOneOffLengthTwoPair (g : ℕ) : Sym2 (Fin (g - 1)) → ℕ × ℕ

The explicit length-two forced inversion attached to an unordered pair.

Equations

• Bananas.crossOneOffLengthTwoPair g = Sym2.lift ⟨fun (a b : Fin (g - 1)) => (2 * min ↑a ↑b + 3, 2 * max ↑a ↑b + 4), ⋯⟩

theorem Bananas.crossOneOffLengthTwoPair_injective (g : ℕ) : Function.Injective (crossOneOffLengthTwoPair g)

theorem Bananas.correctedCrossOneOffForcedCount_le_card_length_two {g : ℕ} (hg : 2 ≤ g) : correctedCrossOneOffForcedCount g 2 ≤ (crossOneOffForcedInversionPairs g 2).card

The corrected n = 2 target is certified by the finite forced block.