Degree-twist deletion identities

The inclusion--exclusion proof of Lemma 4.10 repeatedly removes one or both marked chips from a fixed-degree twist. These elementary identities make the resulting shifts of the finite torsion index explicit.

theorem Bananas.degreeTwistInt_sub_u (M : TwiceMarked) (D : CFDiv M.graph) (d b : ℤ) : degreeTwistInt M D d b - oneChip M.u = degreeTwistInt M D (d - 1) b

Removing the first marked chip lowers the degree-twist index by one.

theorem Bananas.degreeTwistInt_sub_v (M : TwiceMarked) (D : CFDiv M.graph) (d b : ℤ) : degreeTwistInt M D d b - oneChip M.v = degreeTwistInt M D (d - 1) (b + 1)

Removing the second marked chip lowers degree and advances the torsion index by one.

theorem Bananas.degreeTwistInt_sub_uv (M : TwiceMarked) (D : CFDiv M.graph) (d b : ℤ) : degreeTwistInt M D d b - oneChip M.u - oneChip M.v = degreeTwistInt M D (d - 2) (b + 1)

Removing both marked chips lowers degree by two and advances the torsion index once.

theorem Bananas.degreeTwistInt_one_eq_zero_add_u (M : TwiceMarked) (D : CFDiv M.graph) (b : ℤ) : degreeTwistInt M D 1 b = degreeTwistInt M D 0 b + oneChip M.u

The degree-one twists are exactly the first-mark additions of degree-zero twists at the same finite orbit index.