Normalized-coordinate adapter for the verified cross-strand negative-rank calculation.

The normalized/raw coordinate adapter (normalizedPathPosition, strandVertex_eq_pathVertex_normalized, normalizedPathPosition_isInterior) lives in BananaBasics.lean.

theorem Bananas.rank_strand_pair_sub_neg_of_distinct_interior {g : ℕ} (hg : 2 ≤ g) (B : Banana g) (α β γ : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (q : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B γ) (hi : 0 < ↑i ∧ ↑i < B.length α) (hj : 0 < ↑j ∧ ↑j < B.length β) (hq : 0 < ↑q ∧ ↑q < B.length γ) (hαβ : α ≠ β) (hqx : strandVertex B γ q ≠ strandVertex B α i) (hqy : strandVertex B γ q ≠ strandVertex B β j) : rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip (strandVertex B α i) + oneChip (strandVertex B β j) - oneChip (strandVertex B γ q)) = -1