Strong divisibility of sequences from a translation congruence

A sequence a in a GCD domain with a 0 = 0 satisfying the translation congruence a m ∣ a (m + j) - a j for all m, j is a strong divisibility sequence: gcd (a m) (a n) = normalize (a (gcd m n)). Over ℤ this reads Int.gcd (a m) (a n) = |a (gcd m n)|. This is the arithmetic engine behind the Fibonacci-style Int.gcd_fib, isolated from the specific recurrence.

Auxiliary material for the formalization of M. Stoll, Galois groups over ℚ of some iterated polynomials, Arch. Math. 59 (1992), 239-244; upstreaming candidates for Mathlib.

theorem gcd_eq_normalize_of_dvd_sub {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {a : ℕ → R} (h0 : a 0 = 0) (hdvd : ∀ (m j : ℕ), a m ∣ a (m + j) - a j) (m n : ℕ) : gcd (a m) (a n) = normalize (a (m.gcd n))

If a 0 = 0 and a m ∣ a (m + j) - a j for all m, j (the translation congruence), then a is a strong divisibility sequence: gcd (a m) (a n) = normalize (a (gcd m n)).

theorem associated_gcd_of_dvd_sub {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {a : ℕ → R} (h0 : a 0 = 0) (hdvd : ∀ (m j : ℕ), a m ∣ a (m + j) - a j) (m n : ℕ) : Associated (gcd (a m) (a n)) (a (m.gcd n))

The Associated form of gcd_eq_normalize_of_dvd_sub.

theorem Int.gcd_eq_natAbs_of_dvd_sub {a : ℕ → ℤ} (h0 : a 0 = 0) (hdvd : ∀ (m j : ℕ), a m ∣ a (m + j) - a j) (m n : ℕ) : (a m).gcd (a n) = (a (m.gcd n)).natAbs

If a 0 = 0 and a m ∣ a (m + j) - a j for all m, j (the translation congruence), then a is a strong divisibility sequence: Int.gcd (a m) (a n) = |a (gcd m n)|.