Padovan and Perrin sequences

DefinitionShifted Padovan sequence#✓fully proved

The shifted Padovan sequence is the sequence of natural numbers \((a_n)_{n \ge 0}\) with \(a_0 = 1\), \(a_1 = 0\), \(a_2 = 1\) and \(a_{n+3} = a_{n+1} + a_n\) for every \(n \ge 0\).

def shiftedPadovanSequence : Nat → Nat
  | 0 => 1
  | 1 => 0
  | 2 => 1
  | n + 3 => shiftedPadovanSequence (n + 1) + shiftedPadovanSequence n
Sources
Used by 6
Used byCompositions fixed by \(U\) and their Padovan count · Arndt compositions with parts at most 3 and the Padovan numbers · Infinitely many Padovan numbers are not sums of two prime powers · Recurrence of the shifted Padovan sequence · Sum of \(\binom{n+7k}{3n+k}\binom{n}{k} \bmod 2\) as a run length transform · Rampersad–Wiebe Theorem 12

TheoremRecurrence of the shifted Padovan sequence#✓fully proved

For every natural number \(n\), the shifted Padovan sequence \((a_n)_{n \ge 0}\) satisfies \(a_{n+3} = a_{n+1} + a_n\).

theorem shiftedPadovanSequence_add_three (n : Nat) :
    shiftedPadovanSequence (n + 3) =
      shiftedPadovanSequence (n + 1) + shiftedPadovanSequence n
Uses 1
Statement usesShifted Padovan sequence

DefinitionPerrin sequence#✓fully proved

The Perrin sequence \(E_n\), for natural numbers \(n\), is defined by \(E_0 = 3\), \(E_1 = 0\), \(E_2 = 2\) and \(E_n = E_{n-2} + E_{n-3}\) for every \(n \ge 3\).

def perrinSequence : Nat → Nat
  | 0 => 3
  | 1 => 0
  | 2 => 2
  | (n + 3) => perrinSequence (n + 1) + perrinSequence n
Used by 6
Used byThe Perrin sequence and its backward extension fit together at index zero · Negative-index Perrin numbers equal to plus or minus a Perrin square · Perrin numbers that are squares of Perrin numbers · No positive-index Perrin number is the square of a negative-index one · The only zero of the two-sided Perrin sequence · Infinitely many Perrin numbers are not sums of two prime powers
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.