Normal form for a theta counterexample

This connects the general rank-theoretic reduction to the strand geometry.

theorem Bananas.theta_negative_rankDelta_normal_form (B : Banana 2) (u v : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V) (huv : u ≠ v) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (hNeg : rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) u v) D < 0) : ∃! w : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V, linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (D - oneChip u) (oneChip w)

A negative marked second difference on a theta graph has, after deleting the first marked chip, a unique vertex-chip representative.