Rigidity of opposite-factor marks on a genus-one wedge

The phase ell = 0 in the exact wedge rank formula shows that one chip on each factor has rank zero whenever neither chip is the gluing point.

theorem Bananas.rank_wedgeAdd_opposite_one_chips_eq_zero (G : CFGraph) (H : CFGraph) (x u : G.V) (y v : H.V) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hu : u ≠ x) : rank (Utilities.vertexWedge G H x y) (Utilities.wedgeAddDivisor G H x y (oneChip u) (oneChip v)) = 0

One chip on each non-gluing factor vertex has rank zero on the wedge.

theorem Bananas.opposite_wedge_mark_pair_not_linearEquiv_canonical (G : CFGraph) (H : CFGraph) (x u : G.V) (y v : H.V) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hu : u ≠ x) : ¬linearEquiv (Utilities.vertexWedge G H x y) (oneChip (Sum.inl u) + oneChip (Utilities.wedgeRightVertex G H x y v)) (canonicalDivisor (Utilities.vertexWedge G H x y))

Hence the opposite-factor marked pair is not canonical, the rigidity condition used in the distinct-factor branch of Theorem 4.13.