Fibonacci numbers modulo m: periodic zeros and even Pisano periods

For m ≥ 1 the zeros of Fₙ mod m are periodic (m ∣ Fₙ ↔ d ∣ n for the least d > 0 with m ∣ F_d, from gcd(F_a, F_b) = F_gcd(a,b)), the sequence Fₙ mod m is periodic (the pair (Fₙ, Fₙ₊₁) mod m returns to (0, 1): pigeonhole and the invertibility of the recurrence), and for m > 2 every period is even: Cassini's identity F_{π+1} F_{π−1} − F_π² = (−1)^π at a period gives (−1)^π ≡ 1 (mod m) (Singerman's determinant argument).

Main results

• Pisano.dvd_fib_iff: m ∣ Fₙ ↔ d ∣ n for some d > 0
• Pisano.exists_period: Fₙ mod m is periodic
• Pisano.even_of_period: every period is even when m > 2
• Pisano.fib_mod_periodicity: the three parts together (Theorem of the Day)

References

• R. Whitty, Theorem of the Day, «A Theorem on Modular Fibonacci Periodicity» (Binomial/PeriodicFib).
• D. D. Wall, Fibonacci series modulo m, Amer. Math. Monthly 67 (1960), 525–532.

def Pisano.pair (m n : ℕ) : ZMod m × ZMod m

The pair (Fₙ, Fₙ₊₁) in ZMod m.

Equations

• Pisano.pair m n = (↑(Nat.fib n), ↑(Nat.fib (n + 1)))

theorem Pisano.pair_succ (m n : ℕ) : pair m (n + 1) = ((pair m n).2, (pair m n).1 + (pair m n).2)

theorem Pisano.pair_zero (m : ℕ) : pair m 0 = (0, 1)

theorem Pisano.pair_eq_of_succ_eq {m i j : ℕ} (h : pair m (i + 1) = pair m (j + 1)) : pair m i = pair m j

Backward invertibility: equal successors have equal predecessors.

theorem Pisano.exists_return (m : ℕ) [NeZero m] : ∃ (π : ℕ), 0 < π ∧ pair m π = pair m 0

theorem Pisano.exists_period (m : ℕ) (hm : 0 < m) : ∃ (π : ℕ), 0 < π ∧ ∀ (n : ℕ), Nat.fib (n + π) ≡ Nat.fib n [MOD m]

theorem Pisano.dvd_fib_iff (m : ℕ) (hm : 0 < m) : ∃ (d : ℕ), 0 < d ∧ ∀ (n : ℕ), m ∣ Nat.fib n ↔ d ∣ n

theorem Pisano.cassini (n : ℕ) : ↑(Nat.fib (n + 2)) * ↑(Nat.fib n) - ↑(Nat.fib (n + 1)) ^ 2 = (-1) ^ (n + 1)

Cassini in ℤ: F_{n+2} F_n − F_{n+1}² = (−1)^(n+1).

theorem Pisano.even_of_period (m : ℕ) (hm : 2 < m) (π : ℕ) (hπ : 0 < π) (hper : ∀ (n : ℕ), Nat.fib (n + π) ≡ Nat.fib n [MOD m]) : Even π

theorem Pisano.fib_mod_periodicity (m : ℕ) (hm : 0 < m) : (∃ (d : ℕ), 0 < d ∧ ∀ (n : ℕ), m ∣ Nat.fib n ↔ d ∣ n) ∧ (∃ (π : ℕ), 0 < π ∧ ∀ (n : ℕ), Nat.fib (n + π) ≡ Nat.fib n [MOD m]) ∧ (2 < m → ∀ (π : ℕ), 0 < π → (∀ (n : ℕ), Nat.fib (n + π) ≡ Nat.fib n [MOD m]) → Even π)