Exact torsion period API

The definition IsTorsionOrder records minimal positive annihilation. This file derives the group-theoretic consequence used throughout the paper: its period divides every other annihilating period.

theorem Bananas.exists_isTorsionOrder_of_torsionWitness {M : TwiceMarked} {k : ℕ} (hWitness : TorsionWitness M k) : ∃ (n : ℕ), IsTorsionOrder M n

Any positive torsion witness has a least positive witness below it. This is the elementary well-ordering bridge from a period calculation to the paper's exact torsion order.

theorem Bananas.marked_difference_remainder_linearEquiv_zero {M : TwiceMarked} {k m : ℕ} (hk : TorsionWitness M k) (hm : linearEquiv M.graph (↑m • (oneChip M.u - oneChip M.v)) 0) : linearEquiv M.graph ((↑m % ↑k) • (oneChip M.u - oneChip M.v)) 0

The Euclidean remainder of an annihilating marked difference is again principal.

theorem Bananas.isTorsionOrder_dvd_of_torsionWitness {M : TwiceMarked} {k m : ℕ} (hk : IsTorsionOrder M k) (hm : TorsionWitness M m) : k ∣ m

The least positive torsion period divides every other positive torsion period.

theorem Bananas.marked_difference_linearEquiv_zero_of_degreeTwistInt_linearEquiv {M : TwiceMarked} (D : CFDiv M.graph) (d b c : ℤ) (hbc : linearEquiv M.graph (degreeTwistInt M D d b) (degreeTwistInt M D d c)) : linearEquiv M.graph ((b - c) • (oneChip M.u - oneChip M.v)) 0

Linear-equivalent degree twists have an annihilating difference index.

theorem Bananas.isTorsionOrder_dvd_natAbs_sub_of_degreeTwistInt_linearEquiv {M : TwiceMarked} {k : ℕ} (hk : IsTorsionOrder M k) (D : CFDiv M.graph) (d b c : ℤ) (hbc : linearEquiv M.graph (degreeTwistInt M D d b) (degreeTwistInt M D d c)) : k ∣ (b - c).natAbs

At an exact torsion order, two distinct integer degree-twist indices can represent the same class only when their difference is a multiple of the period.

theorem Bananas.degreeTwistInt_injective_on_fundamental_period {M : TwiceMarked} {k : ℕ} (hk : IsTorsionOrder M k) (D : CFDiv M.graph) (d b c : ℤ) (hb0 : 0 ≤ b) (hb : b < ↑k) (hc0 : 0 ≤ c) (hc : c < ↑k) (hbc : linearEquiv M.graph (degreeTwistInt M D d b) (degreeTwistInt M D d c)) : b = c

On one half-open fundamental period, fixed-degree twist representatives are pairwise inequivalent.

theorem Bananas.marked_difference_mod_period_linearEquiv {M : TwiceMarked} {k : ℕ} (hk : TorsionWitness M k) (z : ℤ) : linearEquiv M.graph (z • (oneChip M.u - oneChip M.v)) ((z % ↑k) • (oneChip M.u - oneChip M.v))

A signed marked-difference twist is linearly equivalent to its Euclidean residue modulo any torsion witness.

theorem Bananas.linearEquiv_add_left_of_linearEquiv {G : CFGraph} {A B C : CFDiv G} (hAB : linearEquiv G A B) : linearEquiv G (C + A) (C + B)

Adding a fixed divisor preserves linear equivalence.

theorem Bananas.int_eq_of_emod_sub_eq_zero_of_fundamental {k b c : ℤ} (hk : 0 < k) (hb0 : 0 ≤ b) (hb : b < k) (hc0 : 0 ≤ c) (hc : c < k) (hmod : (b - c) % k = 0) : b = c

In the half-open fundamental interval, congruence modulo a positive period is equality.