Explicit witnesses of recurrence

The paper's recurrence arguments repeatedly exhibit two distinct nonzero torsion residues at which the same degree-one vertex twist is effective. This small generic lemma packages that final finite-residue step.

theorem Bananas.not_nonRecurrent_of_rank_nonneg_one_and_period {M : TwiceMarked} {a k : ℕ} (w : M.graph.V) (haOne : 1 < a) (haK : a < k) (hOne : 0 ≤ rank M.graph (oneChip w + 1 • (oneChip M.u - oneChip M.v))) (hA : 0 ≤ rank M.graph (oneChip w + ↑a • (oneChip M.u - oneChip M.v))) : ¬NonRecurrent M k

Two distinct nonzero effective twists of one vertex disprove nonrecurrence. The residue 1 is singled out because it is the one that arises from the other marked vertex in the vertex-wedge argument.