Basic periodicity lemmas for marked banana transmission

These lemmas are graph-independent. They isolate the part of the paper's torsion-periodicity argument that follows solely from linear equivalence, before any banana rank computation is used.

theorem Bananas.linearEquiv_marked_twist_add_torsion {M : TwiceMarked} {k : ℕ} (hk : TorsionWitness M k) (D : CFDiv M.graph) (a b : ℤ) : linearEquiv M.graph (D + (a + ↑k) • oneChip M.u - (b + ↑k) • oneChip M.v) (D + a • oneChip M.u - b • oneChip M.v)

Simultaneously increasing the two transmission coordinates by a torsion order changes a marked twist by the principal divisor k (u - v).

theorem Bananas.rank_marked_twist_add_torsion {M : TwiceMarked} {k : ℕ} (hk : TorsionWitness M k) (D : CFDiv M.graph) (a b : ℤ) : rank M.graph (D + (a + ↑k) • oneChip M.u - (b + ↑k) • oneChip M.v) = rank M.graph (D + a • oneChip M.u - b • oneChip M.v)

The ranks of corresponding marked twists are periodic at every torsion witness.

theorem Bananas.rankDelta_neg_iff_rank_pattern (M : TwiceMarked) (D : CFDiv M.graph) : rankDelta M D < 0 ↔ rank M.graph D = rank M.graph (D - oneChip M.u) ∧ rank M.graph D = rank M.graph (D - oneChip M.v) ∧ rank M.graph D = rank M.graph (D - oneChip M.u - oneChip M.v) + 1

The only way the marked rank second difference can be negative. This is the rank-pattern criterion used throughout the paper's submodularity proofs.

theorem Bananas.allSubmodular_iff_rankDelta_nonneg (M : TwiceMarked) : AllSubmodular M ↔ ∀ (D : CFDiv M.graph), 0 ≤ rankDelta M D

Because AllSubmodular quantifies over every divisor already, its apparently two-level definition is equivalent to pointwise nonnegativity of the marked rank second difference.

theorem Bananas.not_allSubmodular_iff_exists_rankDelta_neg (M : TwiceMarked) : ¬AllSubmodular M ↔ ∃ (D : CFDiv M.graph), rankDelta M D < 0

Failure of all-divisor submodularity has a single negative rank-difference witness. This is the form used by the theta and higher-genus classifications.