Rigidity of the non-endpoint theta submodularity families

The theta branch of Theorem 4.13 needs the canonical correction in the genus-two inversion formula to vanish. Here that is checked directly from the coordinate families of Corollary 3.6.

theorem Bananas.leftEndpoint_add_not_linearEquiv_canonical (B : Banana 2) (w : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V) (hw : w ≠ rightEndpoint B) : ¬linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip (leftEndpoint B) + oneChip w) (canonicalDivisor (Utilities.Certificate.SubdivisionGraph.Spec.graph B))

Adding a vertex other than the right endpoint to the left endpoint is not canonical on a theta.

theorem Bananas.rightEndpoint_add_not_linearEquiv_canonical (B : Banana 2) (w : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V) (hw : w ≠ leftEndpoint B) : ¬linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip w + oneChip (rightEndpoint B)) (canonicalDivisor (Utilities.Certificate.SubdivisionGraph.Spec.graph B))

Symmetric endpoint version of leftEndpoint_add_not_linearEquiv_canonical.

theorem Bananas.distinctInterior_strand_pair_not_linearEquiv_canonical (B : Banana 2) (alpha beta : Fin 3) (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) (hab : alpha ≠ beta) : ¬linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip (strandVertex B alpha i) + oneChip (strandVertex B beta j)) (canonicalDivisor (Utilities.Certificate.SubdivisionGraph.Spec.graph B))

Two interior chips on distinct theta strands have rank zero, so cannot be canonical.