The reflected theta pair #
On a genus-two banana, a point together with its reflection is a canonical
degree-two divisor. This is the rank-theoretic exclusion used in the
SameStrand argument: a rank-zero pair cannot be a reflected pair.
theorem
Bananas.rank_strand_reflection_pair_eq_one
(B : Banana 2)
(alpha : Fin 3)
(i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha)
:
rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B)
(oneChip (strandVertex B alpha i) + oneChip (strandVertex B alpha (strandMirror B alpha i))) = 1
A point and its reflection on a theta strand have rank exactly one.
theorem
Bananas.ne_strand_reflection_of_pair_rank_zero
(B : Banana 2)
(alpha : Fin 3)
(i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha)
(w : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V)
(hRank : rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip (strandVertex B alpha i) + oneChip w) = 0)
:
Consequently, a rank-zero two-chip divisor cannot pair a point with its strand reflection.