Jacobsthal and Jacobsthal–Lucas numbers

DefinitionJacobsthal–Lucas numbers#✓fully proved

The Jacobsthal–Lucas numbers \(j_0, j_1, j_2, \dots\) are the natural numbers defined by \(j_0 = 2\), \(j_1 = 1\) and \(j_{n+2} = j_{n+1} + 2 j_n\) for all \(n \ge 0\). The sequence begins \(2, 1, 5, 7, 17, \dots\) (OEIS A014551).

def jacobsthalLucasNumber : ℕ → ℕ
  | 0 => 2
  | 1 => 1
  | n + 2 => jacobsthalLucasNumber (n + 1) + 2 * jacobsthalLucasNumber n

Used by 2

Used byJacobsthal–Lucas–Oresme convolution · Powers of two times Jacobsthal–Lucas numbers modulo 9

TheoremJacobsthal closed form#✓fully proved

Let \(J : \mathbb{N} \to \mathbb{N}\) satisfy \(J(0) = J(1) = 1\) and \(J(n+2) = J(n+1) + 2J(n)\) for every \(n \in \mathbb{N}\). Then for every \(m \in \mathbb{N}\),

\[J(m) = \frac{2^{m+1} + (-1)^m}{3}.\]

The source cites A. Tucker, "Applied Combinatorics," 3rd edition, for this formula. The proof applies Binet's formula for second-order linear recurrences; the characteristic polynomial \(x^2 - x - 2\) has roots \(2\) and \(-1\).

theorem jacobsthal_closedForm
    (J : ℕ → ℕ)
    (h_zero : J 0 = 1)
    (h_one : J 1 = 1)
    (h_rec : ∀ n : ℕ, J (n + 2) = J (n + 1) + 2 * J n)
    (m : ℕ) :
    (J m : ℚ) = ((2 : ℚ) ^ (m + 1) + (-1 : ℚ) ^ m) / 3

Sources

• Darrin D. Frey and James A. Sellers, "Jacobsthal Numbers and Alternating Sign Matrices," Journal of Integer Sequences 3 (2000), Article 00.2.3, recurrence with initial values, lines 260–266, and Theorem, equation (Eq4a), lines 329–335, https://cs.uwaterloo.ca/journals/JIS/VOL3/SELLERS/sellers.tex

Uses 1

Proof usesBinet formula for second-order linear recurrences

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.