Second distinct-strand witness in Theorem 3.9

This file proves the second explicit rank witness from the distinct-strand case of corrected Theorem 3.9. In normalized coordinates the second mark is the penultimate point of its strand, while the first mark is not the first interior point. The extra hypothesis 2 < B.length beta excludes precisely the corrected length-two midpoint exception; without it the theorem is false.

theorem Bananas.strand_position_add_penultimate_linearEquiv_right_pred {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (hi : 1 < ↑i) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip (strandVertex B alpha i) + oneChip (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) (oneChip (strandVertex B alpha ⟨↑i - 1, ⋯⟩) + oneChip (rightEndpoint B))

Two normalized chips at positions i and n - 1 slide to position i - 1 and the right endpoint.

theorem Bananas.rankDelta_second_cross_witness_neg {g : ℕ} (hg : 3 ≤ g) (B : Banana g) (alpha beta : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B beta) (hi : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B alpha i) (_hj : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B beta j) (hAlphaBeta : alpha ≠ beta) (hjPenultimate : ↑j + 1 = B.length beta) (hiNotOne : ↑i ≠ 1) (hBetaLength : 2 < B.length beta) : rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha i) (strandVertex B beta j)) (oneChip (strandVertex B alpha i) + oneChip (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩) + oneChip (strandVertex B beta ⟨1, ⋯⟩)) < 0

The second explicit divisor in the distinct-strand proof of corrected Theorem 3.9 has negative rank difference. The length assumption excludes the corrected length-two midpoint exception.

The witness is v_(alpha,i) + v_(alpha,n_alpha-1) + v_(beta,1).