Bi-periodic Fibonacci sequences modulo primes
TheoremPeriod of a generalized bi-periodic Fibonacci sequence modulo a prime, given the roots#✓fully proved
Let \(p\) be an odd prime and let \(a, b, c, d \in \mathbb{Z}/p\mathbb{Z}\) with \(a \ne 0\), \(c \ne 0\), \(d \ne 0\), and \(a \ne b\) or \(c \ne d\). Let \(F : \mathbb{N} \to \mathbb{Z}/p\mathbb{Z}\) satisfy \(F_0 = 0\), \(F_1 = 1\) and, for every \(n \ge 2\), \(F_n = a F_{n-1} + c F_{n-2}\) if \(n\) is even and \(F_n = b F_{n-1} + d F_{n-2}\) if \(n\) is odd. Put \(A = ab + c + d\) and \(\Delta = A^2 - 4cd\), and let \(\alpha, \beta \in \mathbb{Z}/p\mathbb{Z}\) satisfy \(\alpha + \beta = A\) and \(\alpha \beta = cd\). Let \(k\) be the least positive period of \(F\): \(k > 0\), \(F_{n+k} = F_n\) for all \(n\), and \(k \le m\) for every \(m > 0\) with \(F_{n+m} = F_n\) for all \(n\). If \(\Delta \ne 0\), then \(k\) divides \(2(p - 1)\), and if moreover \(\alpha\) and \(\beta\) are nonzero squares in \(\mathbb{Z}/p\mathbb{Z}\), then \(k\) divides \(p - 1\).
Since \(\Delta = (\alpha - \beta)^2\), no hypothesis that \(\Delta\) is a square is needed.
MetaMathlibExt.generalizedBiPeriodicFibonacci_period_dvd_general · 26 lines
theorem generalizedBiPeriodicFibonacci_period_dvd_general :
∀ (p : ℕ) (_hp : p.Prime) (_hpOdd : Odd p)
(a b c d : ZMod p)
(F : ℕ → ZMod p)
(A Δ α β : ZMod p)
(k : ℕ),
F 0 = 0 →
F 1 = 1 →
(∀ n, 2 ≤ n → n % 2 = 0 →
F n = a * F (n - 1) + c * F (n - 2)) →
(∀ n, 2 ≤ n → n % 2 = 1 →
F n = b * F (n - 1) + d * F (n - 2)) →
a ≠ 0 →
c ≠ 0 →
d ≠ 0 →
(a ≠ b ∨ c ≠ d) →
A = a * b + c + d →
Δ = A ^ 2 - 4 * c * d →
α + β = A →
α * β = c * d →
0 < k →
(∀ n, F (n + k) = F n) →
(∀ m, 0 < m → (∀ n, F (n + m) = F n) → k ≤ m) →
Δ ≠ 0 →
k ∣ 2 * (p - 1) ∧
((α ≠ 0 ∧ IsSquare α ∧ β ≠ 0 ∧ IsSquare β) → k ∣ p - 1)TheoremPeriod of a generalized bi-periodic Fibonacci sequence modulo a prime#✓fully proved
Let \(p\) be an odd prime and let \(a, b, c, d \in \mathbb{Z}/p\mathbb{Z}\) with \(a \ne 0\), \(c \ne 0\), \(d \ne 0\), and \(a \ne b\) or \(c \ne d\). Let \(F : \mathbb{N} \to \mathbb{Z}/p\mathbb{Z}\) satisfy \(F_0 = 0\), \(F_1 = 1\) and, for every \(n \ge 2\), \(F_n = a F_{n-1} + c F_{n-2}\) if \(n\) is even and \(F_n = b F_{n-1} + d F_{n-2}\) if \(n\) is odd. Put \(A = ab + c + d\) and \(\Delta = A^2 - 4cd\), and let \(\alpha, \beta \in \mathbb{Z}/p\mathbb{Z}\) satisfy \(\alpha + \beta = A\) and \(\alpha \beta = cd\). Let \(k\) be the least positive period of \(F\): \(k > 0\), \(F_{n+k} = F_n\) for all \(n\), and \(k \le m\) for every \(m > 0\) with \(F_{n+m} = F_n\) for all \(n\). If \(\Delta\) is a nonzero square in \(\mathbb{Z}/p\mathbb{Z}\), then \(k\) divides \(2(p - 1)\), and if moreover \(\alpha\) and \(\beta\) are nonzero squares in \(\mathbb{Z}/p\mathbb{Z}\), then \(k\) divides \(p - 1\).
MetaMathlibExt.generalizedBiPeriodicFibonacci_period_dvd · 27 lines
theorem generalizedBiPeriodicFibonacci_period_dvd :
∀ (p : ℕ) (hp : p.Prime) (hpOdd : Odd p)
(a b c d : ZMod p)
(F : ℕ → ZMod p)
(A Δ α β : ZMod p)
(k : ℕ),
F 0 = 0 →
F 1 = 1 →
(∀ n, 2 ≤ n → n % 2 = 0 →
F n = a * F (n - 1) + c * F (n - 2)) →
(∀ n, 2 ≤ n → n % 2 = 1 →
F n = b * F (n - 1) + d * F (n - 2)) →
a ≠ 0 →
c ≠ 0 →
d ≠ 0 →
(a ≠ b ∨ c ≠ d) →
A = a * b + c + d →
Δ = A ^ 2 - 4 * c * d →
α + β = A →
α * β = c * d →
0 < k →
(∀ n, F (n + k) = F n) →
(∀ m, 0 < m → (∀ n, F (n + m) = F n) → k ≤ m) →
Δ ≠ 0 →
IsSquare Δ →
k ∣ 2 * (p - 1) ∧
((α ≠ 0 ∧ IsSquare α ∧ β ≠ 0 ∧ IsSquare β) → k ∣ p - 1)Sources
- Hacène Belbachir and Celia Salhi, "The Generalized Bi-Periodic Fibonacci Sequence Modulo m," Journal of Integer Sequences 24 (2021), Article 21.9.4, Theorem, lines 225–226, https://cs.uwaterloo.ca/journals/JIS/VOL24/Salhi/salhi4.tex. It follows from
generalizedBiPeriodicFibonacci_period_dvd_general, which drops the unusedIsSquare Δ.
TheoremZero indices of a generalized bi-periodic Fibonacci sequence with \(c = d\)#✓fully proved
Let \(a, b, c, d\) be natural numbers with \(c = d\), and let \(m \ge 2\) be a natural number coprime to \(a\) and to \(c\). Let \((F_n)_{n \ge 0}\) be a sequence of natural numbers with \(F_0 = 0\), \(F_1 = 1\), \(F_{2n+2} = a F_{2n+1} + c F_{2n}\) and \(F_{2n+3} = b F_{2n+2} + d F_{2n+1}\) for all \(n \ge 0\). Then there is an integer \(l > 0\) such that, for every \(n \ge 0\), \(m\) divides \(F_n\) if and only if \(l\) divides \(n\), and \(l \le r\) for every \(r > 0\) such that \(m\) divides \(F_r\).
MetaMathlibExt.generalized_biperiodic_fibonacci_zero_indices_general · 17 lines
theorem generalized_biperiodic_fibonacci_zero_indices_general
{a b c d m : ℕ}
(hm : 2 ≤ m)
(hacoprime : Nat.Coprime a m)
(hccoprime : Nat.Coprime c m)
(hcd : c = d)
(F : ℕ → ℕ)
(hF_zero : F 0 = 0)
(hF_one : F 1 = 1)
(hF_even : ∀ n : ℕ,
F (2 * n + 2) = a * F (2 * n + 1) + c * F (2 * n))
(hF_odd : ∀ n : ℕ,
F (2 * n + 3) = b * F (2 * n + 2) + d * F (2 * n + 1)) :
∃ l : ℕ,
0 < l ∧
(∀ n : ℕ, m ∣ F n ↔ l ∣ n) ∧
(∀ r : ℕ, 0 < r → m ∣ F r → l ≤ r)Uses 2 · Used by 1
TheoremBelbachir–Salhi theorem on zero indices of generalized bi-periodic Fibonacci sequences#✓fully proved
Let \(a, b, c, d\) be positive natural numbers with \(c = d\), and let \(m \ge 2\) be a natural number coprime to \(a\), to \(c\) and to \(d\). Let \((F_n)_{n \ge 0}\) be a sequence of natural numbers with \(F_0 = 0\), \(F_1 = 1\), \(F_{2n+2} = a F_{2n+1} + c F_{2n}\) and \(F_{2n+3} = b F_{2n+2} + d F_{2n+1}\) for all \(n \ge 0\). Then there is a natural number \(l > 0\) such that, for every \(n \ge 0\), \(m\) divides \(F_n\) if and only if \(l\) divides \(n\), and \(l \le r\) for every \(r > 0\) such that \(m\) divides \(F_r\).
The recurrence is \(F_n = a F_{n-1} + c F_{n-2}\) for even \(n \ge 2\) and \(F_n = b F_{n-1} + d F_{n-2}\) for odd \(n \ge 3\). The conditions \(c = d\) and \(\gcd(a, m) = 1\) are the standing assumptions of the source's section, and coprimality of \(c\) and \(d\) with \(m\) is its global hypothesis on the modulus; the positivity of \(a, b, c, d\) and the coprimality of \(d\) with \(m\) are not needed for the conclusion.
MetaMathlibExt.generalized_biperiodic_fibonacci_zero_indices · 19 lines
theorem generalized_biperiodic_fibonacci_zero_indices
{a b c d m : ℕ}
(ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d)
(hm : 2 ≤ m)
(hacoprime : Nat.Coprime a m)
(hccoprime : Nat.Coprime c m)
(hdcoprime : Nat.Coprime d m)
(hcd : c = d)
(F : ℕ → ℕ)
(hF_zero : F 0 = 0)
(hF_one : F 1 = 1)
(hF_even : ∀ n : ℕ,
F (2 * n + 2) = a * F (2 * n + 1) + c * F (2 * n))
(hF_odd : ∀ n : ℕ,
F (2 * n + 3) = b * F (2 * n + 2) + d * F (2 * n + 1)) :
∃ l : ℕ,
0 < l ∧
(∀ n : ℕ, m ∣ F n ↔ l ∣ n) ∧
(∀ r : ℕ, 0 < r → m ∣ F r → l ≤ r)Sources
- Hacène Belbachir and Celia Salhi, "The Generalized Bi-Periodic Fibonacci Sequence Modulo m," Journal of Integer Sequences 24 (2021), Article 21.9.4, Theorem, lines 445–448, https://cs.uwaterloo.ca/journals/JIS/VOL24/Salhi/salhi4.tex
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.