Gibonacci numbers

DefinitionGibonacci numbers#✓fully proved

For integers \(G_0\) and \(G_1\), the Gibonacci sequence with initial values \(G_0\) and \(G_1\) is the integer sequence \((G_n)_{n \ge 0}\) that starts with \(G_0, G_1\) and satisfies \(G_{n+2} = G_{n+1} + G_n\) for every \(n \ge 0\).

def gibonacciNumber (G₀ G₁ : ℤ) : ℕ → ℤ
  | 0 => G₀
  | 1 => G₁
  | n + 2 => gibonacciNumber G₀ G₁ (n + 1) + gibonacciNumber G₀ G₁ n
Used by 18
Used byCounting configurations with long divisibility runs · Divisibility by a Gibonacci sequence forces a Tribonacci sequence to vanish · Growth bounds for Gibonacci and generalized Tribonacci sequences · Backward recurrence for Gibonacci numbers · Gibonacci numbers in terms of Fibonacci numbers · Gibonacci terms two apart have the gcd of the initial values · Divisibility runs · Divisibility runs of length zero · Cassini identity for Gibonacci numbers · Gibonacci numbers starting from 0 and 1 are the Fibonacci numbers · Generating series of a Gibonacci sequence · Good consecutive ratios of a Gibonacci sequence · Consecutive ratios of a shifted Gibonacci sequence are good · Two standard families of good values · Translates of a Gibonacci sequence as composition sums · Subsequences \(G_{\ell n + m}\) of a Gibonacci sequence as composition sums · Multiples of a shifted Gibonacci sequence that are Toeplitz–Hessenberg determinants · Gibonacci subsequences \(G_{2n+m}\) as composition sums

TheoremGibonacci numbers starting from 0 and 1 are the Fibonacci numbers#✓fully proved

For every natural number \(n\), the \(n\)-th Gibonacci number with initial values \(G_0 = 0\) and \(G_1 = 1\) equals the \(n\)-th Fibonacci number \(F_n\) (where \(F_0 = 0\), \(F_1 = 1\) and \(F_{n+2} = F_{n+1} + F_n\)).

theorem gibonacci_zero_one_eq_fib (n : ℕ) :
    gibonacciNumber 0 1 n = (Nat.fib n : ℤ)
Uses 1
Statement usesGibonacci numbers

TheoremCassini identity for Gibonacci numbers#✓fully proved

Let \(G_0\) and \(G_1\) be integers and let \((G_n)\) be the Gibonacci sequence with these initial values, so that \(G_{n+2} = G_{n+1} + G_n\) for all \(n \ge 0\). Then for every natural number \(n \ge 1\), \(G_{n+1} G_{n-1} - G_n^2 = (-1)^n (G_1^2 - G_0 G_1 - G_0^2)\).

theorem gibonacci_cassini_of_pos
    (G₀ G₁ : ℤ) (n : ℕ) (hn : 1 ≤ n) :
    gibonacciNumber G₀ G₁ (n + 1) * gibonacciNumber G₀ G₁ (n - 1) -
      (gibonacciNumber G₀ G₁ n) ^ 2 =
      (-1 : ℤ) ^ n * (G₁ ^ 2 - G₀ * G₁ - G₀ ^ 2)
Sources
  • Guyer and Mbirika, "GCD of Sums of k Consecutive Fibonacci, Lucas, and Generalized Fibonacci Numbers," Journal of Integer Sequences 24 (2021), Article 21.9.8, Proposition 2.5.
Uses 1
Statement usesGibonacci numbers

TheoremMelham's gibonacci sum-of-squares identity, general form#✓fully proved

Let \(G : \mathbb{Z} \to \mathbb{Z}\) satisfy \(G(j+2) = G(j+1) + G(j)\) for every integer \(j\), and let \(F_m\) denote the \(m\)-th Fibonacci number. Then for every integer \(k\) and every natural number \(n\),

\[6\Bigl(\sum_{j=0}^{2n-1} G(k+j)^2\Bigr)^2 = F_{2n}^2\bigl(G(k+n-2)^4 + 4G(k+n-1)^4 + 4G(k+n)^4 + G(k+n+1)^4\bigr).\]

The source states this identity with the additional hypotheses that \(G(0) \ne 0\) or \(G(1) \ne 0\) and that \(n \ge 1\).

theorem melham_fibonacci_gibonacci_sum_of_squares_general
    (G : ℤ → ℤ)
    (hG : ∀ j : ℤ, G (j + 2) = G (j + 1) + G j)
    (k : ℤ) (n : ℕ) :
    6 * (∑ j ∈ Finset.range (2 * n), (G (k + j)) ^ 2) ^ 2 =
      (Nat.fib (2 * n) : ℤ) ^ 2 *
        ((G (k + n - 2)) ^ 4 + 4 * (G (k + n - 1)) ^ 4 +
          4 * (G (k + n)) ^ 4 + (G (k + n + 1)) ^ 4)
Used by 1
Used byMelham's gibonacci sum-of-squares identity

TheoremMelham's gibonacci sum-of-squares identity#✓fully proved

Let \(G : \mathbb{Z} \to \mathbb{Z}\) satisfy \(G(j+2) = G(j+1) + G(j)\) for every integer \(j\), with \(G(0) \ne 0\) or \(G(1) \ne 0\), and let \(F_m\) denote the \(m\)-th Fibonacci number. Then for every integer \(k\) and every natural number \(n \ge 1\),

\[6\Bigl(\sum_{j=0}^{2n-1} G(k+j)^2\Bigr)^2 = F_{2n}^2\bigl(G(k+n-2)^4 + 4G(k+n-1)^4 + 4G(k+n)^4 + G(k+n+1)^4\bigr).\]

The hypotheses \(G(0) \ne 0\) or \(G(1) \ne 0\) and \(n \ge 1\) are not needed; they keep the shape of the source.

theorem melham_fibonacci_gibonacci_sum_of_squares
    (G : ℤ → ℤ)
    (hG : ∀ j : ℤ, G (j + 2) = G (j + 1) + G j)
    (hG_nonzero : G 0 ≠ 0 ∨ G 1 ≠ 0)
    (k : ℤ) (n : ℕ) (hn : 0 < n) :
    6 * (∑ j ∈ Finset.range (2 * n), (G (k + j)) ^ 2) ^ 2 =
      (Nat.fib (2 * n) : ℤ) ^ 2 *
        ((G (k + n - 2)) ^ 4 + 4 * (G (k + n - 1)) ^ 4 +
          4 * (G (k + n)) ^ 4 + (G (k + n + 1)) ^ 4)
Sources
Uses 1
Proof usesMelham's gibonacci sum-of-squares identity, general form

TheoremGibonacci squares recurrence#✓fully proved

Let \(g : \mathbb{N} \to \mathbb{Z}\) satisfy \(g(n+2) = g(n+1) + g(n)\) for every \(n \in \mathbb{N}\), and let \(F_3 = 2\) be the third Fibonacci number. Then for every \(n \in \mathbb{N}\),

\[g(n+3)^2 = F_3\, g(n+2)^2 + F_3\, g(n+1)^2 - g(n)^2.\]

The characteristic polynomial \(x^3 - 2x^2 - 2x + 1\) of this recurrence has roots \(\alpha^2\), \(\beta^2\) and \(-1\), where \(\alpha\) and \(\beta\) are the roots of \(x^2 - x - 1\).

theorem gibonacci_sq_recurrence
    (g : ℕ → ℤ) (hg : ∀ n : ℕ, g (n + 2) = g (n + 1) + g n) (n : ℕ) :
    g (n + 3) ^ 2 = (Nat.fib 3 : ℤ) * g (n + 2) ^ 2 +
      (Nat.fib 3 : ℤ) * g (n + 1) ^ 2 - g n ^ 2
Sources
  • Thomas Koshy, "A Graph-Theoretic Model for a Generalized Fibonacci Gem," Journal of Integer Sequences 22 (2019), Article 19.4.1, Theorem 2, lines 149–153, https://cs.uwaterloo.ca/journals/JIS/VOL22/Koshy/koshy7.tex
6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.