Lamé's theorem on Euclid's algorithm

Lame.euclidSteps a b counts the division steps (a, b) ↦ (b, a mod b) of Euclid's algorithm until b = 0. If the algorithm on (x, y) with y > 0 takes n steps, then F_{n+1} ≤ y (Fibonacci numbers, F_1 = F_2 = 1), with equality at consecutive Fibonacci numbers; since 10^k ≤ F_{5k+2}, n is at most five times the number of decimal digits of y (Lamé, 1844). The proof is a strong induction on b with the invariant F_{n+1} ≤ b and, when b < a, F_{n+2} ≤ a.

Main results

• Lame.fib_euclidSteps_le: F_(n+1) <= y and n <= 5 * (decimal digits of y), n = Euclid steps on (x, y)

References

• G. Lamé, Note sur la limite du nombre des divisions dans la recherche du plus grand commun diviseur entre deux nombres entiers, C. R. Acad. Sci. Paris 19 (1844), 867–870.

@[irreducible]

def Lame.euclidSteps : ℕ → ℕ → ℕ

Number of division steps of Euclid's algorithm on (a, b): (a, b) ↦ (b, a mod b) until b = 0.

Equations

• Lame.euclidSteps x✝ 0 = 0
• Lame.euclidSteps x✝ b.succ = Lame.euclidSteps (b + 1) (x✝ % (b + 1)) + 1

theorem Lame.fib_euclidSteps_le (x y : ℕ) (hy : 0 < y) : Nat.fib (euclidSteps x y + 1) ≤ y ∧ euclidSteps x y ≤ 5 * (Nat.digits 10 y).length

Lamé's theorem (1844). If Euclid's algorithm on (x, y), y > 0, takes n steps, then F_{n+1} ≤ y; hence n is at most five times the number of decimal digits of y.