Cross-strand reduced negative-rank witness #
This is the small, independently useful part of the far-mark calculation.
The reducedness theorem supplies the rank -1 conclusion directly; no
additional rank-zero argument is bundled into it.
theorem
Bananas.cross_strand_rank_minus_one_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 : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B α i)
(hj : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B β j)
(hq : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B γ q)
(hαβ : α ≠ β)
(hqx :
Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B γ q ≠ Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α i)
(hqy :
Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B γ q ≠ Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B β j)
: