Tribonacci numbers

DefinitionTribonacci sequence#✓fully proved

The Tribonacci sequence \((T_n)_{n \ge 0}\) is defined by \(T_0 = 0\), \(T_1 = 0\), \(T_2 = 1\) and \(T_{n+3} = T_{n+2} + T_{n+1} + T_n\) for \(n \ge 0\); it begins \(0, 0, 1, 1, 2, 4, \dots\) (OEIS A000073).

def tribonacci : ℕ → ℕ
  | 0 => 0
  | 1 => 0
  | 2 => 1
  | n + 3 => tribonacci (n + 2) + tribonacci (n + 1) + tribonacci n
Sources
Used by 19
Used byTribonacci formula for a diagonal sum of trinomial coefficients · Tribonacci numbers from every third term of A077943 · Tribonacci approximation error bound · Tribonacci representation · The empty word represents zero · A Tribonacci representation of nine · Late records use \(T_{P(t)}\) and \(T_{Q(t)}\) · Indices used by records of the Tribonacci successor · Partial sums along the positive and negative indices are records · Tribonacci differences do not keep one strict sign for three steps · Tribonacci value of a digit word · The empty digit word has Tribonacci value zero · Row numbers of the Trithoff array · Compositions with parts \(1\), \(2\), \(3\) and the Tribonacci sequence · The Brocard–Ramanujan equation has no Tribonacci solutions · Infinitely many Tribonacci numbers are not sums of two prime powers · The generalized Tribonacci sequence with initial values \(0, 1, 1\) is the shifted Tribonacci sequence · The generalized Tribonacci sequence with initial values \(0, 0, 1\) is the Tribonacci sequence · On nonnegative indices the two-sided Tribonacci sequence is the shifted Tribonacci sequence

DefinitionTribonacci sequence with initial values 1, 1, 1#✓fully proved

The sequence \((T_n)_{n \ge 0}\) of natural numbers defined by \(T_0 = T_1 = T_2 = 1\) and \(T_{n+3} = T_{n+2} + T_{n+1} + T_n\) for every \(n \ge 0\). It begins \(1, 1, 1, 3, 5, 9, 17, \dots\) (OEIS A000213).

def tribonacciWithInitialValues111 : ℕ → ℕ
  | 0 => 1
  | 1 => 1
  | 2 => 1
  | n + 3 =>
      tribonacciWithInitialValues111 (n + 2) +
        tribonacciWithInitialValues111 (n + 1) + tribonacciWithInitialValues111 n
Sources
Used by 1
Used byInteger and natural Tribonacci sequences with initial values \(1, 1, 1\) agree

DefinitionGeneralized Tribonacci sequence#✓fully proved

For integers \(s_0, s_1, s_2\), the generalized Tribonacci sequence \((T_n)_{n \ge 0}\) with initial values \(s_0, s_1, s_2\) is the sequence of integers defined by \(T_0 = s_0\), \(T_1 = s_1\), \(T_2 = s_2\) and \(T_{n+3} = T_{n+2} + T_{n+1} + T_n\) for every \(n \ge 0\).

def generalizedTribonacci (s₀ s₁ s₂ : ℤ) : ℕ → ℤ
  | 0 => s₀
  | 1 => s₁
  | 2 => s₂
  | n + 3 =>
      generalizedTribonacci s₀ s₁ s₂ (n + 2) +
        generalizedTribonacci s₀ s₁ s₂ (n + 1) + generalizedTribonacci s₀ s₁ s₂ n
Sources
  • Gessel–Kar (2024), JIS 27, Article 24.1.3, lines 700–719: T_0 = s₀, T_1 = s₁, T_2 = s₂, and T_{n+3} = T_{n+2} + T_{n+1} + T_n.
Used by 15
Used byRecurrence of the generalized Tribonacci sequence · Initial value \(T_1 = s_1\) of the generalized Tribonacci sequence · Integer and natural Tribonacci sequences with initial values \(1, 1, 1\) agree · Initial value \(T_2 = s_2\) of the generalized Tribonacci sequence · Initial value \(T_0 = s_0\) of the generalized Tribonacci sequence · The generalized Tribonacci sequence with initial values \(0, 1, 1\) is the shifted Tribonacci sequence · The generalized Tribonacci sequence with initial values \(0, 0, 1\) is the Tribonacci sequence · Two-sided Tribonacci sequence · Tribonacci recurrence for the two-sided sequence · Counting configurations with long divisibility runs · Basis sequences for generalized Tribonacci sequences · Divisibility by a Gibonacci sequence forces a Tribonacci sequence to vanish · Growth bounds for Gibonacci and generalized Tribonacci sequences · Divisibility runs · Divisibility runs of length zero

TheoremInitial value \(T_0 = s_0\) of the generalized Tribonacci sequence#✓fully proved

For all integers \(s_0, s_1, s_2\), the generalized Tribonacci sequence \((T_n)_{n \ge 0}\) with initial values \(s_0, s_1, s_2\) satisfies \(T_0 = s_0\).

@[simp] theorem generalizedTribonacci_zero (s₀ s₁ s₂ : ℤ) :
    generalizedTribonacci s₀ s₁ s₂ 0 = s₀
Uses 1
Statement usesGeneralized Tribonacci sequence

TheoremInitial value \(T_1 = s_1\) of the generalized Tribonacci sequence#✓fully proved

For all integers \(s_0, s_1, s_2\), the generalized Tribonacci sequence \((T_n)_{n \ge 0}\) with initial values \(s_0, s_1, s_2\) satisfies \(T_1 = s_1\).

@[simp] theorem generalizedTribonacci_one (s₀ s₁ s₂ : ℤ) :
    generalizedTribonacci s₀ s₁ s₂ 1 = s₁
Uses 1
Statement usesGeneralized Tribonacci sequence

TheoremInitial value \(T_2 = s_2\) of the generalized Tribonacci sequence#✓fully proved

For all integers \(s_0, s_1, s_2\), the generalized Tribonacci sequence \((T_n)_{n \ge 0}\) with initial values \(s_0, s_1, s_2\) satisfies \(T_2 = s_2\).

@[simp] theorem generalizedTribonacci_two (s₀ s₁ s₂ : ℤ) :
    generalizedTribonacci s₀ s₁ s₂ 2 = s₂
Uses 1
Statement usesGeneralized Tribonacci sequence

TheoremRecurrence of the generalized Tribonacci sequence#✓fully proved

For all integers \(s_0, s_1, s_2\) and every \(n \ge 0\), the generalized Tribonacci sequence \((T_n)_{n \ge 0}\) with initial values \(s_0, s_1, s_2\) satisfies \(T_{n+3} = T_{n+2} + T_{n+1} + T_n\).

@[simp] theorem generalizedTribonacci_add_three (s₀ s₁ s₂ : ℤ) (n : ℕ) :
    generalizedTribonacci s₀ s₁ s₂ (n + 3) =
      generalizedTribonacci s₀ s₁ s₂ (n + 2) +
        generalizedTribonacci s₀ s₁ s₂ (n + 1) + generalizedTribonacci s₀ s₁ s₂ n
Uses 1 · Used by 3
Statement usesGeneralized Tribonacci sequence
Used byInteger and natural Tribonacci sequences with initial values \(1, 1, 1\) agree · The generalized Tribonacci sequence with initial values \(0, 1, 1\) is the shifted Tribonacci sequence · The generalized Tribonacci sequence with initial values \(0, 0, 1\) is the Tribonacci sequence

TheoremThe generalized Tribonacci sequence with initial values \(0, 0, 1\) is the Tribonacci sequence#✓fully proved

The generalized Tribonacci sequence with initial values \(0, 0, 1\) is the Tribonacci sequence. For every \(n \ge 0\), the \(n\)-th term of the generalized Tribonacci sequence with initial values \(0, 0, 1\) equals the \(n\)-th Tribonacci number \(t_n\) (where \(t_0 = t_1 = 0\) and \(t_2 = 1\)), viewed as an integer.

theorem generalizedTribonacci_zero_zero_one_eq_tribonacci (n : ℕ) :
    generalizedTribonacci 0 0 1 n = (tribonacci n : ℤ)
Uses 3
Statement usesGeneralized Tribonacci sequence · Tribonacci sequence
Proof usesRecurrence of the generalized Tribonacci sequence

TheoremInteger and natural Tribonacci sequences with initial values \(1, 1, 1\) agree#✓fully proved

For every \(n \ge 0\), the \(n\)-th term of the generalized Tribonacci sequence with initial values \(1, 1, 1\) equals the \(n\)-th term of the Tribonacci sequence of natural numbers with initial values \(1, 1, 1\), viewed as an integer.

theorem generalizedTribonacci_one_one_one_eq_tribonacciWithInitialValues111 (n : ℕ) :
    generalizedTribonacci 1 1 1 n = (tribonacciWithInitialValues111 n : ℤ)
Uses 3
Statement usesGeneralized Tribonacci sequence · Tribonacci sequence with initial values 1, 1, 1
Proof usesRecurrence of the generalized Tribonacci sequence

TheoremThe generalized Tribonacci sequence with initial values \(0, 1, 1\) is the shifted Tribonacci sequence#✓fully proved

The generalized Tribonacci sequence with initial values \(0, 1, 1\) is the shifted Tribonacci sequence. For every \(n \ge 0\), the \(n\)-th term of the generalized Tribonacci sequence with initial values \(0, 1, 1\) equals the Tribonacci number \(t_{n+1}\), viewed as an integer, where \(t_0 = t_1 = 0\) and \(t_2 = 1\).

The initial values \(0, 1, 1\) are the usual Tribonacci convention used by Gessel–Kar; since the Tribonacci sequence \(t\) starts \(0, 0, 1\), the index shift by one is needed.

theorem generalizedTribonacci_zero_one_one_eq_tribonacci_succ (n : ℕ) :
    generalizedTribonacci 0 1 1 n = (tribonacci (n + 1) : ℤ)
Uses 3 · Used by 1
Statement usesGeneralized Tribonacci sequence · Tribonacci sequence
Proof usesRecurrence of the generalized Tribonacci sequence
Used byOn nonnegative indices the two-sided Tribonacci sequence is the shifted Tribonacci sequence

DefinitionBackward half of the two-sided Tribonacci sequence#✓fully proved

The integer sequence \((B_m)_{m \ge 0}\) is defined by \(B_0 = 0\), \(B_1 = 0\), \(B_2 = 1\) and \(B_{m+3} = B_m - B_{m+1} - B_{m+2}\) for every \(m \ge 0\).

Writing \(B_m = T_{-m}\), the initial values are \(T_0 = 0\), \(T_{-1} = 0\), \(T_{-2} = 1\), and the recursion is the Tribonacci recurrence \(T_{n+3} = T_{n+2} + T_{n+1} + T_n\) solved for \(T_n\).

public def tribonacciBackward : ℕ → ℤ
  | 0 => 0
  | 1 => 0
  | 2 => 1
  | m + 3 =>
      tribonacciBackward m - tribonacciBackward (m + 1) - tribonacciBackward (m + 2)
Sources
  • Paul Thomas Young, On the Brocard-Ramanujan Equation with Tribonacci and Tetranacci Numbers, INTEGERS 24 (2024), Article A92, Proposition 1.
Used by 2
Used byTwo-sided Tribonacci sequence · Tribonacci recurrence for the two-sided sequence

DefinitionTwo-sided Tribonacci sequence#✓fully proved

The integer sequence \((T_n)_{n \in \mathbb{Z}}\) is defined on the nonnegative indices by \(T_0 = 0\), \(T_1 = T_2 = 1\) and \(T_{n+3} = T_{n+2} + T_{n+1} + T_n\) for \(n \ge 0\), and on the negative indices by \(T_{-1} = 0\), \(T_{-2} = 1\) and \(T_{-m-3} = T_{-m} - T_{-m-1} - T_{-m-2}\) for \(m \ge 0\), the recurrence solved for its lowest term.

public def tribonacciInt : ℤ → ℤ
  | .ofNat n => generalizedTribonacci 0 1 1 n
  | .negSucc m => tribonacciBackward (m + 1)
Sources
  • Paul Thomas Young, On the Brocard-Ramanujan Equation with Tribonacci and Tetranacci Numbers, INTEGERS 24 (2024), Article A92, Proposition 1.
Uses 2 · Used by 11
Statement usesGeneralized Tribonacci sequence · Backward half of the two-sided Tribonacci sequence
Used byThe Tribonacci number of index \(-10\) · The \(47\)-adic valuation of Tribonacci numbers near \(\pm 1\) · Tribonacci recurrence for the two-sided sequence · On nonnegative indices the two-sided Tribonacci sequence is the shifted Tribonacci sequence · The two-sided Tribonacci sequence at \(-1\) · The two-sided Tribonacci sequence at \(-7\) · The two-sided Tribonacci sequence at \(-3\) · The two-sided Tribonacci sequence at \(-2\) · The two-sided Tribonacci sequence at \(1\) · The two-sided Tribonacci sequence at \(2\) · The two-sided Tribonacci sequence at \(0\)

TheoremThe two-sided Tribonacci sequence at \(0\)#✓fully proved

Let \((T_n)_{n \in \mathbb{Z}}\) be the two-sided Tribonacci sequence: \(T_0 = 0\), \(T_1 = T_2 = 1\) and \(T_{n+3} = T_{n+2} + T_{n+1} + T_n\) for \(n \ge 0\), while \(T_{-1} = 0\), \(T_{-2} = 1\) and \(T_{-m-3} = T_{-m} - T_{-m-1} - T_{-m-2}\) for \(m \ge 0\). Then \(T_0 = 0\).

This is the first initial value used by Proposition 1.

public theorem tribonacciInt_zero : tribonacciInt 0 = 0
Sources
  • Paul Thomas Young, On the Brocard-Ramanujan Equation with Tribonacci and Tetranacci Numbers, INTEGERS 24 (2024), Article A92, Proposition 1.
Uses 1
Statement usesTwo-sided Tribonacci sequence

TheoremThe two-sided Tribonacci sequence at \(1\)#✓fully proved

Let \((T_n)_{n \in \mathbb{Z}}\) be the two-sided Tribonacci sequence: \(T_0 = 0\), \(T_1 = T_2 = 1\) and \(T_{n+3} = T_{n+2} + T_{n+1} + T_n\) for \(n \ge 0\), while \(T_{-1} = 0\), \(T_{-2} = 1\) and \(T_{-m-3} = T_{-m} - T_{-m-1} - T_{-m-2}\) for \(m \ge 0\). Then \(T_1 = 1\).

This is one of Proposition 1's five indices at which the value lies in \(\{\pm 1\}\).

public theorem tribonacciInt_one : tribonacciInt 1 = 1
Sources
  • Paul Thomas Young, On the Brocard-Ramanujan Equation with Tribonacci and Tetranacci Numbers, INTEGERS 24 (2024), Article A92, Proposition 1.
Uses 1
Statement usesTwo-sided Tribonacci sequence

TheoremThe two-sided Tribonacci sequence at \(2\)#✓fully proved

Let \((T_n)_{n \in \mathbb{Z}}\) be the two-sided Tribonacci sequence: \(T_0 = 0\), \(T_1 = T_2 = 1\) and \(T_{n+3} = T_{n+2} + T_{n+1} + T_n\) for \(n \ge 0\), while \(T_{-1} = 0\), \(T_{-2} = 1\) and \(T_{-m-3} = T_{-m} - T_{-m-1} - T_{-m-2}\) for \(m \ge 0\). Then \(T_2 = 1\).

This is one of Proposition 1's five indices at which the value lies in \(\{\pm 1\}\).

public theorem tribonacciInt_two : tribonacciInt 2 = 1
Sources
  • Paul Thomas Young, On the Brocard-Ramanujan Equation with Tribonacci and Tetranacci Numbers, INTEGERS 24 (2024), Article A92, Proposition 1.
Uses 1
Statement usesTwo-sided Tribonacci sequence

TheoremThe two-sided Tribonacci sequence at \(-1\)#✓fully proved

Let \((T_n)_{n \in \mathbb{Z}}\) be the two-sided Tribonacci sequence: \(T_0 = 0\), \(T_1 = T_2 = 1\) and \(T_{n+3} = T_{n+2} + T_{n+1} + T_n\) for \(n \ge 0\), while \(T_{-1} = 0\), \(T_{-2} = 1\) and \(T_{-m-3} = T_{-m} - T_{-m-1} - T_{-m-2}\) for \(m \ge 0\). Then \(T_{-1} = 0\).

This fixes the first value across the boundary between negative and nonnegative indices.

public theorem tribonacciInt_neg_one : tribonacciInt (-1) = 0
Sources
  • Paul Thomas Young, On the Brocard-Ramanujan Equation with Tribonacci and Tetranacci Numbers, INTEGERS 24 (2024), Article A92, Proposition 1.
Uses 1
Statement usesTwo-sided Tribonacci sequence

TheoremThe two-sided Tribonacci sequence at \(-2\)#✓fully proved

Let \((T_n)_{n \in \mathbb{Z}}\) be the two-sided Tribonacci sequence: \(T_0 = 0\), \(T_1 = T_2 = 1\) and \(T_{n+3} = T_{n+2} + T_{n+1} + T_n\) for \(n \ge 0\), while \(T_{-1} = 0\), \(T_{-2} = 1\) and \(T_{-m-3} = T_{-m} - T_{-m-1} - T_{-m-2}\) for \(m \ge 0\). Then \(T_{-2} = 1\).

This is one of Proposition 1's five indices at which the value lies in \(\{\pm 1\}\).

public theorem tribonacciInt_neg_two : tribonacciInt (-2) = 1
Sources
  • Paul Thomas Young, On the Brocard-Ramanujan Equation with Tribonacci and Tetranacci Numbers, INTEGERS 24 (2024), Article A92, Proposition 1.
Uses 1
Statement usesTwo-sided Tribonacci sequence

TheoremThe two-sided Tribonacci sequence at \(-3\)#✓fully proved

Let \((T_n)_{n \in \mathbb{Z}}\) be the two-sided Tribonacci sequence: \(T_0 = 0\), \(T_1 = T_2 = 1\) and \(T_{n+3} = T_{n+2} + T_{n+1} + T_n\) for \(n \ge 0\), while \(T_{-1} = 0\), \(T_{-2} = 1\) and \(T_{-m-3} = T_{-m} - T_{-m-1} - T_{-m-2}\) for \(m \ge 0\). Then \(T_{-3} = -1\).

This is one of Proposition 1's five indices at which the value lies in \(\{\pm 1\}\).

public theorem tribonacciInt_neg_three : tribonacciInt (-3) = -1
Sources
  • Paul Thomas Young, On the Brocard-Ramanujan Equation with Tribonacci and Tetranacci Numbers, INTEGERS 24 (2024), Article A92, Proposition 1.
Uses 1
Statement usesTwo-sided Tribonacci sequence

TheoremThe two-sided Tribonacci sequence at \(-7\)#✓fully proved

Let \((T_n)_{n \in \mathbb{Z}}\) be the two-sided Tribonacci sequence: \(T_0 = 0\), \(T_1 = T_2 = 1\) and \(T_{n+3} = T_{n+2} + T_{n+1} + T_n\) for \(n \ge 0\), while \(T_{-1} = 0\), \(T_{-2} = 1\) and \(T_{-m-3} = T_{-m} - T_{-m-1} - T_{-m-2}\) for \(m \ge 0\). Then \(T_{-7} = 1\).

This is one of Proposition 1's five indices at which the value lies in \(\{\pm 1\}\).

public theorem tribonacciInt_neg_seven : tribonacciInt (-7) = 1
Sources
  • Paul Thomas Young, On the Brocard-Ramanujan Equation with Tribonacci and Tetranacci Numbers, INTEGERS 24 (2024), Article A92, Proposition 1.
Uses 1
Statement usesTwo-sided Tribonacci sequence

TheoremTribonacci recurrence for the two-sided sequence#✓fully proved

Let \((T_n)_{n \in \mathbb{Z}}\) be the two-sided Tribonacci sequence: \(T_0 = 0\), \(T_1 = T_2 = 1\) and \(T_{n+3} = T_{n+2} + T_{n+1} + T_n\) for \(n \ge 0\), while \(T_{-1} = 0\), \(T_{-2} = 1\) and \(T_{-m-3} = T_{-m} - T_{-m-1} - T_{-m-2}\) for \(m \ge 0\). Then \(T_{n+3} = T_{n+2} + T_{n+1} + T_n\) for every integer \(n\), including the three indices \(n = -3, -2, -1\) at which the recurrence crosses zero.

public theorem tribonacciInt_add_three (n : ℤ) :
    tribonacciInt (n + 3) =
      tribonacciInt (n + 2) + tribonacciInt (n + 1) + tribonacciInt n
Sources
  • Paul Thomas Young, On the Brocard-Ramanujan Equation with Tribonacci and Tetranacci Numbers, INTEGERS 24 (2024), Article A92, Proposition 1.
Uses 3
Statement usesTwo-sided Tribonacci sequence
Proof usesGeneralized Tribonacci sequence · Backward half of the two-sided Tribonacci sequence

TheoremOn nonnegative indices the two-sided Tribonacci sequence is the shifted Tribonacci sequence#✓fully proved

On nonnegative indices the two-sided Tribonacci sequence is the shifted Tribonacci sequence. Let \((T_n)_{n \in \mathbb{Z}}\) be the two-sided Tribonacci sequence: \(T_0 = 0\), \(T_1 = T_2 = 1\) and \(T_{n+3} = T_{n+2} + T_{n+1} + T_n\) for \(n \ge 0\), while \(T_{-1} = 0\), \(T_{-2} = 1\) and \(T_{-m-3} = T_{-m} - T_{-m-1} - T_{-m-2}\) for \(m \ge 0\). Let \((t_n)_{n \ge 0}\) be the Tribonacci sequence with \(t_0 = t_1 = 0\), \(t_2 = 1\) and \(t_{n+3} = t_{n+2} + t_{n+1} + t_n\). Then \(T_n = t_{n+1}\) for every natural number \(n\).

This is the bridge between Proposition 1's normalization and Theorem 1's natural-indexed sequence.

public theorem tribonacciInt_nat_eq (n : ℕ) :
    tribonacciInt (n : ℤ) = (tribonacci (n + 1) : ℤ)
Sources
  • Paul Thomas Young, On the Brocard-Ramanujan Equation with Tribonacci and Tetranacci Numbers, INTEGERS 24 (2024), Article A92, Theorem 1 and Proposition 1 notation.
Uses 3
Statement usesTribonacci sequence · Two-sided Tribonacci sequence
Proof usesThe generalized Tribonacci sequence with initial values \(0, 1, 1\) is the shifted Tribonacci sequence
21 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.