Degree bookkeeping for twice-marked twists

Transmission inequalities repeatedly use divisors of the form D + a • oneChip u - b • oneChip v. This module isolates the elementary degree identities so later formalizations do not repeatedly unfold CFDiv.degree and fight integer casts.

theorem Utilities.deg_seam_difference {G : CFGraph} (u v : G.V) : CFDiv.degree (oneChip u - oneChip v) = 0

The marked difference u-v has degree zero.

theorem Utilities.deg_zsmul_seam_difference {G : CFGraph} (u v : G.V) (n : ℤ) : CFDiv.degree (n • (oneChip u - oneChip v)) = 0

Integral multiples of a marked difference preserve degree.

theorem Utilities.deg_add_marked_twist {G : CFGraph} (D : CFDiv G) (u v : G.V) (a b : ℤ) : CFDiv.degree (D + a • oneChip u - b • oneChip v) = CFDiv.degree D + a - b

Exact degree of a two-marked twist.

theorem Utilities.deg_add_zsmul_seam {G : CFGraph} (D : CFDiv G) (u v : G.V) (n : ℤ) : CFDiv.degree (D + n • (oneChip u - oneChip v)) = CFDiv.degree D

Translating by the seam direction does not change degree.

theorem Utilities.deg_add_marked_twist_of_degree {G : CFGraph} (D : CFDiv G) (u v : G.V) (a b d : ℤ) (hDegree : CFDiv.degree D = d) : CFDiv.degree (D + a • oneChip u - b • oneChip v) = d + a - b

The transmission convention D + a u - b v has the expected affine change in degree. This variant is useful when the base degree is known.