Pisano periods

TheoremFulton–Morris theorem on Pisano periods equal to the modulus#✓fully proved

Write \(F_t\) for the \(t\)-th Fibonacci number. Let \(m > 1\) be a natural number and let \(\pi\) be a positive integer with \(F_\pi \equiv 0 \pmod{m}\) and \(F_{\pi+1} \equiv 1 \pmod{m}\) such that \(\pi \le t\) for every positive integer \(t\) with \(F_t \equiv 0 \pmod{m}\) and \(F_{t+1} \equiv 1 \pmod{m}\); that is, \(\pi\) is the Pisano period of \(m\). Then \(\pi = m\) if and only if \(m = 24 \cdot 5^{\lambda - 1}\) for some integer \(\lambda \ge 1\).

theorem fulton_morris_pisano_fixed_point
    (m period : ℕ) (hm : 1 < m) (hperiod : 0 < period)
    (hreturn : Nat.ModEq m (Nat.fib period) 0 ∧
      Nat.ModEq m (Nat.fib (period + 1)) 1)
    (hleast : ∀ t : ℕ, 0 < t →
      Nat.ModEq m (Nat.fib t) 0 → Nat.ModEq m (Nat.fib (t + 1)) 1 →
      period ≤ t) :
    period = m ↔ ∃ lambda : ℕ, 0 < lambda ∧ m = 24 * 5 ^ (lambda - 1)
Sources
  • Amirali Fatehizadeh and Daniel Yaqubi, "Average of the Fibonacci Numbers," Journal of Integer Sequences 25 (2022), Article 22.2.6, https://cs.uwaterloo.ca/journals/JIS/VOL25/Yaqubi/yaq6.tex, lines 177–189. The theorem is attributed there to John Fulton and William Morris, "On arithmetical functions related to the Fibonacci numbers," Acta Arithmetica 16 (1969), 105–110, DOI 10.4064/aa-16-2-105-110.
Uses 2
Proof usesFibonacci prime divisibility · The \(5\)-adic valuation of Fibonacci numbers

DefinitionPisano period#✓fully proved

For a natural number \(n\), the Pisano period \(\pi(n)\) is the minimal period of the pair \((0, 1)\) under the Fibonacci step \((a, b) \mapsto (b, a + b)\) on \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/n\mathbb{Z}\): the least \(k \ge 1\) such that \(k\) applications of the step map \((0, 1)\) back to \((0, 1)\), or \(0\) if there is no such \(k\) (as for \(n = 0\), where \(\mathbb{Z}/0\mathbb{Z} = \mathbb{Z}\)).

noncomputable def pisanoPeriod (n : ℕ) : ℕ :=
  Function.minimalPeriod
    (fun p : ZMod n × ZMod n => (p.2, p.1 + p.2)) (0, 1)
Used by 2
Used byThe Pisano period of \(F_n\) divides \(2n\) for even \(n\) · The minimum of \(\pi(n)/n\) over \(1 \le n < N\) tends to zero

TheoremThe Pisano period of \(F_n\) divides \(2n\) for even \(n\)#●ready to prove

Let \(F_n\) denote the \(n\)-th Fibonacci number and \(\pi(m)\) the Pisano period of \(m\). For every even natural number \(n > 1\), \(\pi(F_n)\) divides \(2n\).

theorem_wanted pisanoPeriod_fib_dvd_two_mul
    (n : ℕ) (hn : 1 < n) (hn2 : 2 ∣ n) :
    pisanoPeriod (Nat.fib n) ∣ 2 * n
Sources
  • Oisín Flynn-Connolly, "On the Divisibility of Sums of Fibonacci Numbers", Proposition 2.
Uses 1
Statement usesPisano period

TheoremThe minimum of \(\pi(n)/n\) over \(1 \le n < N\) tends to zero#●ready to prove

Let \(\pi(n)\) denote the Pisano period of \(n\). As \(N \to \infty\), the minimum of the real numbers \(\pi(n)/n\) over the integers \(1 \le n \le N - 1\) (defined for \(N \ge 2\)) tends to \(0\).

theorem_wanted tendsto_iInf_pisanoPeriod_div_atTop
    :
    Filter.Tendsto
      (fun N : ℕ =>
        ⨅ n : {n : ℕ // n ∈ Finset.Icc 1 (N - 1)},
          (pisanoPeriod n.1 : ℝ) / n.1)
      Filter.atTop (nhds 0)
Sources
  • Oisín Flynn-Connolly, "On the Divisibility of Sums of Fibonacci Numbers", Corollary 1.
Uses 1
Statement usesPisano period

TheoremSum of the first \(p\) Fibonacci numbers modulo a prime \(p\)#●ready to prove

Let \(p > 5\) be a prime, let \(F_i\) denote the \(i\)-th Fibonacci number, with \(F_1 = F_2 = 1\), and let \(S = F_1 + F_2 + \dots + F_p\). If \(p \equiv 1\) or \(4 \pmod 5\), then \(S\) leaves remainder \(1\) on division by \(p\); if \(p \equiv 2\) or \(3 \pmod 5\), then \(S\) leaves remainder \(p - 2\) on division by \(p\); and in every case \(p\) does not divide \(S\).

theorem_wanted sum_fib_mod_prime_eq_and_not_dvd
    (p : ℕ) (hp : p.Prime) (hp5 : 5 < p) :
    ((p % 5 = 1 ∨ p % 5 = 4) →
        (∑ i ∈ Finset.Icc 1 p, Nat.fib i) % p = 1) ∧
      ((p % 5 = 2 ∨ p % 5 = 3) →
        (∑ i ∈ Finset.Icc 1 p, Nat.fib i) % p = p - 2) ∧
      ¬p ∣ (∑ i ∈ Finset.Icc 1 p, Nat.fib i)
Sources
  • Oisín Flynn-Connolly, "On the Divisibility of Sums of Fibonacci Numbers", Theorem 1.

TheoremOdd Fibonacci numbers \(F_n\) with \(F_{F_n + 2} \equiv 1 \pmod{F_n}\)#●ready to prove

Let \(F_m\) denote the \(m\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\). If \(p\) is an odd prime with \(p \equiv 2 \pmod 3\) and \(p \equiv 2\) or \(3 \pmod 5\), and \(n = 2p\) or \(n = 4p\), then \(F_n\) is odd and \(F_{F_n + 2}\) leaves remainder \(1\) on division by \(F_n\).

theorem_wanted fib_two_mul_prime_odd_and_fib_fib_add_two_mod
    (p n : ℕ) (hp : p.Prime) (hpodd : p % 2 = 1)
    (hp3 : p % 3 = 2) (hp5 : p % 5 = 2 ∨ p % 5 = 3)
    (hn : n = 2 * p ∨ n = 4 * p) :
    Nat.fib n % 2 = 1 ∧
      Nat.fib (Nat.fib n + 2) % Nat.fib n = 1
Sources
  • Oisín Flynn-Connolly, "On the Divisibility of Sums of Fibonacci Numbers", Theorem 2.

TheoremInfinitely many odd \(k\) divide the sum of the first \(k\) Fibonacci numbers#●ready to prove

Let \(F_i\) denote the \(i\)-th Fibonacci number, with \(F_1 = F_2 = 1\). There are infinitely many odd positive integers \(k\) such that \(k\) divides \(F_1 + F_2 + \dots + F_k\).

theorem_wanted infinite_setOf_odd_dvd_sum_fib
    :
    {k : ℕ | Odd k ∧ k ∣ (∑ i ∈ Finset.Icc 1 k, Nat.fib i)}.Infinite
Sources
  • Oisín Flynn-Connolly, "On the Divisibility of Sums of Fibonacci Numbers", Corollary 2.
2 fully proved5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.