Nonrecurrence and canonical rank supports

This is the finite-residue formulation of Lemma 4.7 in the twice-marked banana paper. On a connected genus-two graph, Riemann--Roch identifies an effective degree-one marked twist with membership of its vertex in the rank support of the canonical complementary twist. Consequently the paper's nonrecurrence condition is exactly pairwise disjointness of those canonical supports.

theorem Bananas.mem_rankSupport_canonical_sub_markedTwist_iff {M : TwiceMarked} (hconn : _root_.graphConnected M.graph) (hgenus : M.graph.genus = 2) (w : M.graph.V) (n : ℕ) : w ∈ rankSupport M.graph (canonicalDivisor M.graph - ↑n • (oneChip M.u - oneChip M.v)) ↔ 0 ≤ rank M.graph (oneChip w + ↑n • (oneChip M.u - oneChip M.v))

A degree-one marked twist is effective exactly when its vertex belongs to the rank support of the corresponding canonical complementary twist.

def Bananas.CanonicalMarkedSupportsPairwiseDisjoint (M : TwiceMarked) (k : ℕ) : Prop

The canonical supports indexed by two distinct nonzero residues are disjoint.

Equations

• One or more equations did not get rendered due to their size.

theorem Bananas.nonRecurrent_iff_canonicalMarkedSupportsPairwiseDisjoint {M : TwiceMarked} {k : ℕ} (hconn : _root_.graphConnected M.graph) (hgenus : M.graph.genus = 2) : NonRecurrent M k ↔ CanonicalMarkedSupportsPairwiseDisjoint M k

Lemma 4.7: nonrecurrence is equivalent to pairwise disjointness of the canonical support complexes of the nonzero marked twists.