Leonardo p-numbers

DefinitionInitial values of the generalized Leonardo \(p\)-numbers#✓fully proved

For natural numbers \(p\), \(k\) and \(n\), this is the list of integers \((\mathcal{L}_{p,k}(0), \mathcal{L}_{p,k}(1), \dots, \mathcal{L}_{p,k}(n))\) of length \(n + 1\), where \(\mathcal{L}_{p,k}(i) = 1\) for \(0 \le i \le p\) and \(\mathcal{L}_{p,k}(i) = \mathcal{L}_{p,k}(i-1) + \mathcal{L}_{p,k}(i-p-1) + k\) for \(i > p\).

def leonardoPKSeq (p k : ℕ) : ℕ → List ℤ
  | 0 => [1]
  | n + 1 =>
      let prev := leonardoPKSeq p k n
      prev ++ [if n + 1 ≤ p then 1
        else prev.getD n 0 + prev.getD (n - p) 0 + (k : ℤ)]

Used by 1

Used byGeneralized Leonardo \(p\)-numbers

DefinitionGeneralized Leonardo \(p\)-numbers#✓fully proved

For natural numbers \(p\) and \(k\), the generalized Leonardo \(p\)-numbers are the integers \(\mathcal{L}_{p,k}(n)\), \(n \in \mathbb{N}\), given by \(\mathcal{L}_{p,k}(n) = 1\) for \(0 \le n \le p\) and \(\mathcal{L}_{p,k}(n) = \mathcal{L}_{p,k}(n-1) + \mathcal{L}_{p,k}(n-p-1) + k\) for \(n > p\).

def leonardoPK (p k n : ℕ) : ℤ := (leonardoPKSeq p k n).getD n 0

Uses 1 · Used by 12

Statement usesInitial values of the generalized Leonardo \(p\)-numbers

Used byCounting Leonardo \(p\)-tilings · Recurrence for the hyper Leonardo \(p\)-numbers · Generalized Leonardo \(p\)-numbers in terms of Fibonacci \(p\)-numbers · Leonardo p-numbers split into incomplete and hyper parts · Honsberger-type identity for generalized Leonardo \(p\)-numbers · Homogeneous recurrence for the Leonardo \(p\)-numbers · Generalized Leonardo \(p\)-numbers at integer arguments · Lucas-Leonardo \(p\)-numbers from Leonardo \(p\)-numbers · Sums of \(p+1\) consecutive Fibonacci \(p\)-numbers · Partial sums of the generalized Leonardo \(p\)-numbers · Stride sums of the generalized Leonardo \(p\)-numbers · Generalized Leonardo numbers as Leonardo \(p\)-numbers with \(p = 1\)

DefinitionForward evaluation of the \(H(p)\) recurrence#✓fully proved

For a natural number \(p\), a function \(s : \mathbb{Z} \to \mathbb{Z}\) and \(n \in \mathbb{N}\), this is the list of the \(2p + n + 1\) values at \(-p, -p+1, \dots, p+n\) (the entry at position \(i\) is the value at \(i - p\)) of the sequence \(H\) that equals \(s\) on \([-p, p]\) and continues by the \(H(p)\) recurrence \(H(t) = H(t-1) + H(t-p) - H(t-2p-1)\) for \(t > p\). Each step appends one value to the previous list, so evaluation takes polynomial time.

For \(p = 0\), where this rule is circular, every appended value is \(0\).

def hSeqForward (seedA : ℤ → ℤ) (p : ℕ) : ℕ → List ℤ
  | 0 => (List.range (2 * p + 1)).map fun i => seedA ((i : ℤ) - p)
  | n + 1 =>
      let prev := hSeqForward seedA p n
      prev ++ [prev.getD (2 * p + n) 0 + prev.getD (p + 1 + n) 0 -
        prev.getD n 0]

Used by 1

Used byTwo-sided extension of initial values by the \(H(p)\) recurrence

DefinitionBackward evaluation of the \(H(p)\) recurrence#✓fully proved

For a natural number \(p\), a function \(s : \mathbb{Z} \to \mathbb{Z}\) and \(n \in \mathbb{N}\), this is the list of the values at \(-p-n, \dots, p\) of the sequence \(H\) that equals \(s\) on \([-p, p]\) and continues to the left by \(H(t) = H(t+2p) + H(t+p+1) - H(t+2p+1)\) for \(t < -p\), which is the \(H(p)\) recurrence \(H(u) = H(u-1) + H(u-p) - H(u-2p-1)\) at \(u = t+2p+1\) solved for \(H(t)\). Each step prepends one value to the previous list.

For \(p = 0\), where this rule is circular, every prepended value equals \(s(0)\).

def hSeqBackward (seedA : ℤ → ℤ) (p : ℕ) : ℕ → List ℤ
  | 0 => (List.range (2 * p + 1)).map fun i => seedA ((i : ℤ) - p)
  | n + 1 =>
      let prev := hSeqBackward seedA p n
      (prev.getD (2 * p - 1) 0 + prev.getD p 0 - prev.getD (2 * p) 0) ::
        prev

Used by 1

Used byTwo-sided extension of initial values by the \(H(p)\) recurrence

DefinitionTwo-sided extension of initial values by the \(H(p)\) recurrence#✓fully proved

For a natural number \(p \ge 1\) and a function \(s : \mathbb{Z} \to \mathbb{Z}\), this is the unique function \(H : \mathbb{Z} \to \mathbb{Z}\) that agrees with \(s\) on \([-p, p]\) and satisfies \(H(t) = H(t-1) + H(t-p) - H(t-2p-1)\) for every integer \(t\): its values at \(t > p\) are computed forward and its values at \(t < -p\) backward from this recurrence. For \(p = 0\) its value is \(s(0)\) at every \(t \le 0\) and \(0\) at every \(t > 0\).

def hSeqZ (seedA : ℤ → ℤ) (p : ℕ) (z : ℤ) : ℤ :=
  if -(p : ℤ) ≤ z then
    (hSeqForward seedA p (z + p).toNat).getD (z + p).toNat 0
  else
    (hSeqBackward seedA p (-(z + p)).toNat).getD 0 0

Uses 2 · Used by 2

Statement usesBackward evaluation of the \(H(p)\) recurrence · Forward evaluation of the \(H(p)\) recurrence

Used byThe sequence \(A_p\) · The two-sided sequence \(B_p\)

DefinitionThe sequence \(A_p\)#✓fully proved

For a natural number \(p \ge 1\), \(A_p : \mathbb{Z} \to \mathbb{Z}\) is the unique sequence with \(A_p(n) = 0\) for \(-p \le n \le 0\) and \(A_p(n) = 1\) for \(1 \le n \le p\) that satisfies \(A_p(n) = A_p(n-1) + A_p(n-p) - A_p(n-2p-1)\) for every integer \(n\). For \(p = 0\) it is the zero sequence.

def seqAZ (p : ℕ) (z : ℤ) : ℤ :=
  hSeqZ (fun w => if w ≤ 0 then 0 else 1) p z

Uses 1 · Used by 6

Statement usesTwo-sided extension of initial values by the \(H(p)\) recurrence

Used byFibonacci \(p\)-numbers as differences of \(A_p\) · Convolution identity for sequences in \(H(p)\) · Entry formula for the powers of \(Q_p\) · Relation between the sequences \(A_p\) and \(B_p\) · The sequence \(A_p\) as a sum of Fibonacci \(p\)-numbers · Recurrence for the sequence \(A_p\)

DefinitionThe two-sided sequence \(B_p\)#✓fully proved

For a natural number \(p \ge 1\), the sequence \(B_p\) of integers indexed by \(\mathbb{Z}\) is the unique solution of the recurrence \(B_p(n) = B_p(n-1) + B_p(n-p) - B_p(n-2p-1)\) for every integer \(n\) (the defining recurrence of the paper's class \(H(p)\)) with initial values \(B_p(n) = 1\) for \(1 \le n \le p\), \(B_p(-p+1) = 1\), and \(B_p(n) = 0\) for the other integers \(n\) with \(-p \le n \le 0\).

The definition also accepts \(p = 0\), where the recurrence is trivial and the construction has no mathematical meaning.

def seqBZ (p : ℕ) (z : ℤ) : ℤ :=
  hSeqZ (fun w => if w ≤ 0 then (if w = -(p : ℤ) + 1 then 1 else 0)
    else 1) p z

Uses 1 · Used by 4

Statement usesTwo-sided extension of initial values by the \(H(p)\) recurrence

Used byConvolution identity for sequences in \(H(p)\) · Entry formula for the powers of \(Q_p\) · Relation between the sequences \(A_p\) and \(B_p\) · Recurrence for the sequence \(B_p\)

DefinitionThe companion matrix \(Q_p\)#✓fully proved

For a natural number \(p\), \(Q_p\) is the \((2p+1) \times (2p+1)\) integer matrix with rows and columns indexed by \(0, 1, \dots, 2p\) whose entry \((2p, 0)\) is \(-1\), whose other entries \((0, 0)\), \((p-1, 0)\) and \((i, i+1)\) for \(0 \le i < 2p\) are \(1\), and whose remaining entries are \(0\).

def companionQ (p : ℕ) : Matrix (Fin (2 * p + 1)) (Fin (2 * p + 1)) ℤ :=
  Matrix.of fun i j =>
    if j.val = 0 ∧ i.val = 2 * p then -1
    else if (j.val = 0 ∧ (i.val = 0 ∨ i.val = p - 1)) ∨
        j.val = i.val + 1 then 1
    else 0

Used by 2

Used byEntries of the powers of the companion matrix \(Q_p\) · Powers of \(Q_p\) shift the Hankel matrices \(R_{p,m}\)

DefinitionEntry formula for the powers of \(Q_p\)#✓fully proved

For natural numbers \(p\) and \(n\) and indices \(a, b \in \{0, 1, \dots, 2p\}\), the value is the integer \(A_p(n + 1 - b)\) if \(a = 0\), the integer \(B_p(n - p + 1 + a - b)\) if \(1 \le a \le p - 1\), and the integer \(-A_p(n - 2p + a - b)\) otherwise, where \(A_p\) and \(B_p\) are the two-sided auxiliary sequences of the generalized Leonardo \(p\)-numbers.

This is the formula of Theorem 9 of the source for the \((a, b)\) entry of \(Q_p^n\), where \(p \ge 2\) and \(Q_p\) is the \((2p+1) \times (2p+1)\) companion matrix of the source, with the index direction along the \(B_p\) rows corrected (the source's display reverses it after the first entry).

def qPowEntry (p n : ℕ) (a b : Fin (2 * p + 1)) : ℤ :=
  if a.val = 0 then seqAZ p ((n : ℤ) + 1 - b.val)
  else if a.val ≤ p - 1 then seqBZ p ((n : ℤ) - p + 1 + a.val - b.val)
  else -seqAZ p ((n : ℤ) - (2 * p - a.val) - b.val)

Uses 2 · Used by 1

Statement usesThe sequence \(A_p\) · The two-sided sequence \(B_p\)

Used byEntries of the powers of the companion matrix \(Q_p\)

DefinitionThe Hankel matrix \(R_{p,m}\)#✓fully proved

For a natural number \(p\), a sequence \(H : \mathbb{Z} \to \mathbb{Z}\) and a natural number \(m\), \(R_{p,m}\) is the \((2p+1) \times (2p+1)\) integer matrix, with rows and columns indexed by \(0, 1, \dots, 2p\), whose \((a, b)\) entry is \(H(m - a - b)\).

def rMatrix (p : ℕ) (H : ℤ → ℤ) (m : ℕ) :
    Matrix (Fin (2 * p + 1)) (Fin (2 * p + 1)) ℤ :=
  Matrix.of fun a b => H ((m : ℤ) - a.val - b.val)

Used by 1

Used byPowers of \(Q_p\) shift the Hankel matrices \(R_{p,m}\)

TheoremGeneralized Leonardo \(p\)-numbers in terms of Fibonacci \(p\)-numbers#●ready to prove

For all natural numbers \(p\), \(k\) and \(n\) with \(p \ge 1\) and \(k \ge 1\), the generalized Leonardo \(p\)-number \(\mathcal{L}_{p,k}(n)\) and the Fibonacci \(p\)-number \(F_p(n+1)\) satisfy \(\mathcal{L}_{p,k}(n) = (k+1)F_p(n+1) - k\).

theorem_wanted leonardoPK_eq (p k n : ℕ) (hp : 1 ≤ p)
    (hk : 1 ≤ k) :
    leonardoPK p k n = ((k : ℤ) + 1) * (MetaMathlibExt.fibonacciP p (n + 1) : ℤ) - (k : ℤ)

Sources

• "On Generalized Leonardo p-Numbers", Journal of Integer Sequences 27 (2024), Article 24.4.6, Theorem 2.

Uses 2

Statement usesGeneralized Leonardo \(p\)-numbers · Fibonacci p-numbers

TheoremPartial sums of the generalized Leonardo \(p\)-numbers#●ready to prove

Let \(p \ge 1\) and \(k \ge 1\) be natural numbers, and let \(\mathcal{L}_{p,k}\) denote the generalized Leonardo \(p\)-numbers (\(\mathcal{L}_{p,k}(j) = 1\) for \(0 \le j \le p\) and \(\mathcal{L}_{p,k}(j) = \mathcal{L}_{p,k}(j-1) + \mathcal{L}_{p,k}(j-p-1) + k\) for \(j > p\)). Then for every natural number \(n\), \(\sum_{i=0}^{n} \mathcal{L}_{p,k}(i) = \mathcal{L}_{p,k}(n+p+1) - k(n+1) - 1\).

theorem_wanted sum_leonardoPK (p k n : ℕ) (hp : 1 ≤ p)
    (hk : 1 ≤ k) :
    ∑ i ∈ Finset.range (n + 1), leonardoPK p k i =
      leonardoPK p k (n + p + 1) - (k : ℤ) * (n + 1) - 1

Sources

• "On Generalized Leonardo p-Numbers", Journal of Integer Sequences 27 (2024), Article 24.4.6, Theorem 3.

Uses 1

Statement usesGeneralized Leonardo \(p\)-numbers

TheoremStride sums of the generalized Leonardo \(p\)-numbers#●ready to prove

Let \(p \ge 1\) and \(k \ge 1\) be natural numbers, and let \(\mathcal{L}_{p,k}\) denote the generalized Leonardo \(p\)-numbers (\(\mathcal{L}_{p,k}(j) = 1\) for \(0 \le j \le p\) and \(\mathcal{L}_{p,k}(j) = \mathcal{L}_{p,k}(j-1) + \mathcal{L}_{p,k}(j-p-1) + k\) for \(j > p\)). Then for all natural numbers \(m \le p\) and \(n\), the sum \(S = \sum_{i=0}^{n} \mathcal{L}_{p,k}((p+1)i + m)\) satisfies \(S = \mathcal{L}_{p,k}((p+1)n + m + 1) - kn\) if \(m < p\), and \(S = \mathcal{L}_{p,k}((p+1)(n+1)) - k(n+1) - 1\) if \(m = p\).

theorem_wanted sum_leonardoPK_stride (p k m n : ℕ)
    (hp : 1 ≤ p) (hk : 1 ≤ k) (hm : m ≤ p) :
    ∑ i ∈ Finset.range (n + 1), leonardoPK p k ((p + 1) * i + m) =
      if m < p then
        leonardoPK p k ((p + 1) * n + m + 1) - (k : ℤ) * n
      else
        leonardoPK p k ((p + 1) * (n + 1)) - (k : ℤ) * (n + 1) - 1

Sources

• "On Generalized Leonardo p-Numbers", Journal of Integer Sequences 27 (2024), Article 24.4.6, Theorem 4.

Uses 1

Statement usesGeneralized Leonardo \(p\)-numbers

TheoremFibonacci \(p\)-numbers as differences of \(A_p\)#●ready to prove

For all natural numbers \(p \ge 1\) and \(n \ge 1\), the Fibonacci \(p\)-number \(F_p(n)\) equals \(A_p(n) - A_p(n-p)\). Here \(A_p : \mathbb{Z} \to \mathbb{Z}\) is the sequence with \(A_p(t) = 0\) for \(-p \le t \le 0\), \(A_p(t) = 1\) for \(1 \le t \le p\), and \(A_p(t) = A_p(t-1) + A_p(t-p) - A_p(t-2p-1)\) for every integer \(t\).

theorem_wanted fibonacciP_eq_seqAZ_sub (p n : ℕ) (hp : 1 ≤ p)
    (hn : 1 ≤ n) :
    (MetaMathlibExt.fibonacciP p n : ℤ) = seqAZ p (n : ℤ) - seqAZ p ((n : ℤ) - p)

Sources

• "On Generalized Leonardo p-Numbers", Journal of Integer Sequences 27 (2024), Article 24.4.6, Theorem 5.

Uses 2

Statement usesThe sequence \(A_p\) · Fibonacci p-numbers

TheoremThe sequence \(A_p\) as a sum of Fibonacci \(p\)-numbers#●ready to prove

For natural numbers \(p\), \(j\) and \(m\) with \(j < p\), the auxiliary sequence \(A_p\) and the Fibonacci \(p\)-numbers \(F_p\) satisfy \(A_p(mp + j) = \sum_{i=0}^{m} F_p(ip + j)\).

theorem_wanted seqAZ_eq_sum_fibonacciP (p j m : ℕ) (hp : 1 ≤ p)
    (hj : j < p) :
    seqAZ p ((m * p + j : ℕ) : ℤ) =
      ∑ i ∈ Finset.range (m + 1), (MetaMathlibExt.fibonacciP p (i * p + j) : ℤ)

Sources

• "On Generalized Leonardo p-Numbers", Journal of Integer Sequences 27 (2024), Article 24.4.6, Corollary 6.

Uses 2

Statement usesThe sequence \(A_p\) · Fibonacci p-numbers

TheoremRecurrence for the sequence \(A_p\)#●ready to prove

For natural numbers \(p \ge 2\) and \(n \ge 1\), the auxiliary sequence \(A_p\) satisfies \(A_p(n) = A_p(n-1) + A_p(n-p-1) + 1\) if \(n \equiv 1 \pmod p\), and \(A_p(n) = A_p(n-1) + A_p(n-p-1)\) otherwise.

theorem_wanted seqAZ_recurrence (p n : ℕ) (hp : 2 ≤ p)
    (hn : 1 ≤ n) :
    seqAZ p (n : ℤ) =
      seqAZ p ((n : ℤ) - 1) + seqAZ p ((n : ℤ) - p - 1) +
        (if n % p = 1 % p then 1 else 0)

Sources

• "On Generalized Leonardo p-Numbers", Journal of Integer Sequences 27 (2024), Article 24.4.6, Proposition 7.

Uses 1

Statement usesThe sequence \(A_p\)

TheoremRecurrence for the sequence \(B_p\)#●ready to prove

For natural numbers \(p \ge 2\) and \(n \ge 1\), the auxiliary sequence \(B_p\) satisfies \(B_p(n) = B_p(n-1) + B_p(n-p-1) + \varepsilon\), where \(\varepsilon = 1\) if \(n \equiv 1 \pmod p\), \(\varepsilon = -1\) if \(n \equiv 2 \pmod p\), and \(\varepsilon = 0\) otherwise. For \(p = 2\) this means \(\varepsilon = 1\) for odd \(n\) and \(\varepsilon = -1\) for even \(n\).

theorem_wanted seqBZ_recurrence (p n : ℕ) (hp : 2 ≤ p)
    (hn : 1 ≤ n) :
    seqBZ p (n : ℤ) =
      seqBZ p ((n : ℤ) - 1) + seqBZ p ((n : ℤ) - p - 1) +
        (if n % p = 1 % p then 1 else if n % p = 2 % p then -1 else 0)

Sources

• "On Generalized Leonardo p-Numbers", Journal of Integer Sequences 27 (2024), Article 24.4.6, Proposition 7.

Uses 1

Statement usesThe two-sided sequence \(B_p\)

TheoremRelation between the sequences \(A_p\) and \(B_p\)#●ready to prove

For natural numbers \(p \ge 2\) and \(n\), the auxiliary sequences \(A_p\) and \(B_p\) satisfy \(A_p(n) = B_p(n+1) - 1\) if \(p\) divides \(n\), and \(A_p(n) = B_p(n+1)\) otherwise.

theorem_wanted seqAZ_eq_seqBZ (p n : ℕ) (hp : 2 ≤ p) :
    seqAZ p (n : ℤ) =
      if n % p = 0 then seqBZ p ((n : ℤ) + 1) - 1
      else seqBZ p ((n : ℤ) + 1)

Sources

• "On Generalized Leonardo p-Numbers", Journal of Integer Sequences 27 (2024), Article 24.4.6, Proposition 8.

Uses 2

Statement usesThe sequence \(A_p\) · The two-sided sequence \(B_p\)

TheoremEntries of the powers of the companion matrix \(Q_p\)#●ready to prove

Let \(p \ge 2\) and \(n\) be natural numbers, and index the rows and columns of the \((2p+1) \times (2p+1)\) companion matrix \(Q_p\) by \(0, 1, \dots, 2p\). Then for all indices \(a\) and \(b\), the entry \((a, b)\) of \(Q_p^n\) equals \(A_p(n + 1 - b)\) if \(a = 0\), equals \(B_p(n - p + 1 + a - b)\) if \(1 \le a \le p - 1\), and equals \(-A_p(n - (2p - a) - b)\) if \(p \le a \le 2p\). Here \(A_p, B_p : \mathbb{Z} \to \mathbb{Z}\) are the sequences satisfying \(S(t) = S(t-1) + S(t-p) - S(t-2p-1)\) for every integer \(t\), with \(A_p(t) = 1\) for \(1 \le t \le p\) and \(A_p(t) = 0\) for \(-p \le t \le 0\), and with \(B_p(t) = 1\) for \(1 \le t \le p\) and for \(t = -p+1\) and \(B_p(t) = 0\) for the other \(-p \le t \le 0\).

theorem_wanted companionQ_pow_apply (p n : ℕ) (hp : 2 ≤ p)
    (a b : Fin (2 * p + 1)) :
    (companionQ p ^ n) a b = qPowEntry p n a b

Sources

• "On Generalized Leonardo p-Numbers", Journal of Integer Sequences 27 (2024), Article 24.4.6, Theorem 9.

Uses 2

Statement usesThe companion matrix \(Q_p\) · Entry formula for the powers of \(Q_p\)

TheoremPowers of \(Q_p\) shift the Hankel matrices \(R_{p,m}\)#●ready to prove

Let \(p \ge 2\) be a natural number and let \(H : \mathbb{Z} \to \mathbb{Z}\) satisfy \(H(t) = H(t-1) + H(t-p) - H(t-2p-1)\) for every integer \(t\). For a natural number \(m\), let \(R_{p,m}\) be the \((2p+1) \times (2p+1)\) integer matrix whose \((a, b)\) entry is \(H(m - a - b)\) for \(0 \le a, b \le 2p\), and let \(Q_p\) be the \((2p+1) \times (2p+1)\) companion matrix with entries \(1\) at \((0, 0)\), at \((p-1, 0)\) and on the superdiagonal, \(-1\) at \((2p, 0)\), and \(0\) elsewhere. Then \(R_{p,m} Q_p^n = R_{p,m+n}\) for all natural numbers \(m \ge 1\) and \(n\).

theorem_wanted rMatrix_mul_companionQ_pow (p : ℕ) (hp : 2 ≤ p)
    (H : ℤ → ℤ)
    (hH : ∀ n : ℤ, H n = H (n - 1) + H (n - p) - H (n - 2 * p - 1))
    (m n : ℕ) (hm : 1 ≤ m) :
    rMatrix p H m * companionQ p ^ n = rMatrix p H (m + n)

Sources

• "On Generalized Leonardo p-Numbers", Journal of Integer Sequences 27 (2024), Article 24.4.6, Theorem 10.

Uses 2

Statement usesThe companion matrix \(Q_p\) · The Hankel matrix \(R_{p,m}\)

TheoremConvolution identity for sequences in \(H(p)\)#●ready to prove

Let \(p \ge 2\) be a natural number and let \(\mathcal{H} : \mathbb{Z} \to \mathbb{Z}\) be a sequence in \(H(p)\), that is, \(\mathcal{H}(t) = \mathcal{H}(t-1) + \mathcal{H}(t-p) - \mathcal{H}(t-2p-1)\) for every integer \(t\). Then for all natural numbers \(m \ge 1\) and \(n \ge 1\),

\[ \mathcal{H}(m+n) = \mathcal{H}(m)A_p(n+1) + \sum_{i=1}^{p-1} \mathcal{H}(m-i)B_p(n-p+i+1) - \sum_{i=0}^{p} \mathcal{H}(m-p-i)A_p(n-p+i), \]

where \(A_p, B_p : \mathbb{Z} \to \mathbb{Z}\) are the sequences in \(H(p)\) with \(A_p(t) = 1\) for \(1 \le t \le p\) and \(A_p(t) = 0\) for \(-p \le t \le 0\), and with \(B_p(t) = 1\) for \(1 \le t \le p\) and for \(t = -p+1\) and \(B_p(t) = 0\) for the other \(-p \le t \le 0\).

theorem_wanted h_add_eq (p : ℕ) (hp : 2 ≤ p) (H : ℤ → ℤ)
    (hH : ∀ n : ℤ, H n = H (n - 1) + H (n - p) - H (n - 2 * p - 1))
    (m n : ℕ) (hm : 1 ≤ m) (hn : 1 ≤ n) :
    H ((m : ℤ) + n) =
      H (m : ℤ) * seqAZ p ((n : ℤ) + 1) +
        ∑ i ∈ Finset.Icc 1 (p - 1), H ((m : ℤ) - i) *
          seqBZ p ((n : ℤ) - p + i + 1) -
        ∑ i ∈ Finset.range (p + 1), H ((m : ℤ) - p - i) *
          seqAZ p ((n : ℤ) - p + i)

Sources

• "On Generalized Leonardo p-Numbers", Journal of Integer Sequences 27 (2024), Article 24.4.6, Corollary 11.

Uses 2

Statement usesThe sequence \(A_p\) · The two-sided sequence \(B_p\)

TheoremSums of \(p+1\) consecutive Fibonacci \(p\)-numbers#●ready to prove

Let \(p \ge 1\) and \(n \ge 1\) be natural numbers and let \(k\) be a natural number. Let \(F_p\) denote the Fibonacci \(p\)-numbers (\(F_p(0) = 0\), \(F_p(m) = 1\) for \(1 \le m \le p\), and \(F_p(m) = F_p(m-1) + F_p(m-p-1)\) for \(m > p\)), and let \(\mathcal{L}_{p,k}\) denote the generalized Leonardo \(p\)-numbers (\(\mathcal{L}_{p,k}(m) = 1\) for \(0 \le m \le p\) and \(\mathcal{L}_{p,k}(m) = \mathcal{L}_{p,k}(m-1) + \mathcal{L}_{p,k}(m-p-1) + k\) for \(m > p\)). Then \((k+1) \sum_{i=0}^{p} F_p(n+i) = \mathcal{L}_{p,k}(n+2p-1) + k\).

theorem_wanted succ_mul_sum_fibonacciP (p k n : ℕ) (hp : 1 ≤ p)
    (hn : 1 ≤ n) :
    ((k : ℤ) + 1) * ∑ i ∈ Finset.range (p + 1), (MetaMathlibExt.fibonacciP p (n + i) : ℤ) =
      leonardoPK p k (n + 2 * p - 1) + (k : ℤ)

Sources

• "On Generalized Leonardo p-Numbers", Journal of Integer Sequences 27 (2024), Article 24.4.6, Lemma 12.

Uses 2

Statement usesGeneralized Leonardo \(p\)-numbers · Fibonacci p-numbers

DefinitionGeneralized Leonardo \(p\)-numbers at integer arguments#✓fully proved

For natural numbers \(p\) and \(k\) and an integer \(z\), the value is the generalized Leonardo \(p\)-number \(\mathcal{L}_{p,k}(z)\) if \(z \ge 0\), and \(-k\) if \(z < 0\).

For \(-p \le z \le -1\) these are the values \(\mathcal{L}_{p,k}(z) = -k\) obtained by running the recurrence \(\mathcal{L}_{p,k}(n) = \mathcal{L}_{p,k}(n-1) + \mathcal{L}_{p,k}(n-p-1) + k\) backwards; below \(-p\) they need not be, but Theorem 13 of the source only uses arguments \(z \ge -p\).

def leonardoPKZ (p k : ℕ) (z : ℤ) : ℤ :=
  if 0 ≤ z then leonardoPK p k z.toNat else -(k : ℤ)

Uses 1 · Used by 2

Statement usesGeneralized Leonardo \(p\)-numbers

Used byHonsberger-type identity for generalized Leonardo \(p\)-numbers · Lucas-Leonardo \(p\)-numbers from Leonardo \(p\)-numbers

TheoremHonsberger-type identity for generalized Leonardo \(p\)-numbers#●ready to prove

Let \(p\), \(k\), \(m\) and \(n\) be natural numbers with \(p, k, m, n \ge 1\). Write \(\mathcal{L}\) for the generalized Leonardo \(p\)-numbers \(\mathcal{L}_{p,k}\), extended to negative integers by \(\mathcal{L}(t) = -k\) for \(t < 0\). Then

\[ \mathcal{L}(m)\mathcal{L}(n+1) + \sum_{i=1}^{p} \mathcal{L}(m-i)\mathcal{L}(n-p+i) = (k+1)\mathcal{L}(m+n+1) - k\bigl(\mathcal{L}(m+p) + \mathcal{L}(n+p+1)\bigr) + pk^2 + k. \]

The arguments that occur are at least \(-p\), and on \([-p, -1]\) the value \(-k\) is the one forced by the recurrence \(\mathcal{L}(t) = \mathcal{L}(t-1) + \mathcal{L}(t-p-1) + k\) read backwards. The paper prints the summation index as \(j\) in \(\mathcal{L}(m-j)\); it is corrected to \(i\) here.

theorem_wanted leonardoPK_honsberger (p k m n : ℕ)
    (hp : 1 ≤ p) (hk : 1 ≤ k) (hm : 1 ≤ m) (hn : 1 ≤ n) :
    leonardoPK p k m * leonardoPK p k (n + 1) +
        ∑ i ∈ Finset.Icc 1 p, leonardoPKZ p k ((m : ℤ) - i) *
          leonardoPKZ p k ((n : ℤ) - p + i) =
      ((k : ℤ) + 1) * leonardoPK p k (m + n + 1) -
        (k : ℤ) * (leonardoPK p k (m + p) +
          leonardoPK p k (n + p + 1)) +
        (p : ℤ) * k ^ 2 + (k : ℤ)

Sources

• "On Generalized Leonardo p-Numbers", Journal of Integer Sequences 27 (2024), Article 24.4.6, Theorem 13.

Uses 2

Statement usesGeneralized Leonardo \(p\)-numbers · Generalized Leonardo \(p\)-numbers at integer arguments

DefinitionLucas-type recurrence lists#✓fully proved

Let \(\alpha\) be a type with a zero, a one and an addition, let \(p\) be a natural number and let \(a_0, c \in \alpha\). Define \(a_i = 1\) for \(1 \le i \le p\) and \(a_n = a_{n-1} + a_{n-p-1} + c\) for \(n > p\). For every natural number \(n\), the Lucas-type list with parameters \(p\), \(a_0\), \(c\) ending at index \(n\) is \([a_0, a_1, \dots, a_n]\).

The list is built by appending one value per step, so each earlier value is computed once and evaluation is quadratic in \(n\), not exponential as with the naive two-branch recursion. The Lucas and Lucas-Leonardo \(p\)-numbers are the cases \(c = 0\) and \(c = p\).

def lucasTypeSeq {α : Type*} [Zero α] [One α] [Add α] (p : ℕ) (a₀ c : α) : ℕ → List α
  | 0 => [a₀]
  | n + 1 =>
      let prev := lucasTypeSeq p a₀ c n
      prev ++ [if n + 1 ≤ p then 1 else prev.getD n 0 + prev.getD (n - p) 0 + c]

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Section 1, display (5).

Used by 9

Used byLucas-Leonardo \(p\)-numbers · Lucas-Leonardo \(p\)-numbers at indices \(1\) to \(p\) · Recurrence for the Lucas-Leonardo \(p\)-numbers · Lucas \(p\)-numbers · Lucas \(p\)-numbers at indices \(1\) to \(p\) · Recurrence for the Lucas \(p\)-numbers · Entries of a Lucas-type list do not depend on its length · Last entry of a Lucas-type list · Length of a Lucas-type list

TheoremLength of a Lucas-type list#✓fully proved

For every type \(\alpha\) with a zero, a one and an addition, every natural number \(p\), all \(a_0, c \in \alpha\) and every natural number \(n\), the Lucas-type list with parameters \(p\), \(a_0\), \(c\) ending at index \(n\) has exactly \(n + 1\) entries.

theorem lucasTypeSeq_length {α : Type*} [Zero α] [One α] [Add α] (p : ℕ) (a₀ c : α)
    (n : ℕ) : (lucasTypeSeq p a₀ c n).length = n + 1

Sources

• Belkhir and Tan, INTEGERS 25 (2025), Article A57, Section 1.

Uses 1 · Used by 2

Statement usesLucas-type recurrence lists

Used byEntries of a Lucas-type list do not depend on its length · Last entry of a Lucas-type list

TheoremEntries of a Lucas-type list do not depend on its length#✓fully proved

Let \(\alpha\) be a type with a zero, a one and an addition, let \(p\) be a natural number and let \(a_0, c \in \alpha\). For natural numbers \(i \le n\), the entry at index \(i\) of the Lucas-type list with parameters \(p\), \(a_0\), \(c\) ending at index \(n\) equals the entry at index \(i\) of the Lucas-type list ending at index \(i\).

theorem lucasTypeSeq_getD {α : Type*} [Zero α] [One α] [Add α] (p : ℕ) (a₀ c : α)
    {i n : ℕ} (h : i ≤ n) :
    (lucasTypeSeq p a₀ c n).getD i 0 = (lucasTypeSeq p a₀ c i).getD i 0

Sources

• Belkhir and Tan, INTEGERS 25 (2025), Article A57, Section 1.

Uses 2 · Used by 1

Statement usesLucas-type recurrence lists

Proof usesLength of a Lucas-type list

Used byLast entry of a Lucas-type list

TheoremLast entry of a Lucas-type list#✓fully proved

Let \(\alpha\) be a type with a zero, a one and an addition, let \(p\) be a natural number and let \(a_0, c \in \alpha\). Write \(S_m\) for the Lucas-type list with parameters \(p\), \(a_0\), \(c\) ending at index \(m\), and \(S_m[i]\) for its entry at index \(i\). Then for every natural number \(n\), \(S_{n+1}[n+1] = 1\) if \(n + 1 \le p\), and otherwise \(S_{n+1}[n+1] = S_n[n] + S_{n-p}[n-p] + c\).

theorem lucasTypeSeq_getD_succ {α : Type*} [Zero α] [One α] [Add α] (p : ℕ) (a₀ c : α)
    (n : ℕ) :
    (lucasTypeSeq p a₀ c (n + 1)).getD (n + 1) 0 =
      if n + 1 ≤ p then 1
      else (lucasTypeSeq p a₀ c n).getD n 0 +
        (lucasTypeSeq p a₀ c (n - p)).getD (n - p) 0 + c

Sources

• Belkhir and Tan, INTEGERS 25 (2025), Article A57, Section 1.

Uses 3 · Used by 4

Statement usesLucas-type recurrence lists

Proof usesEntries of a Lucas-type list do not depend on its length · Length of a Lucas-type list

Used byLucas-Leonardo \(p\)-numbers at indices \(1\) to \(p\) · Recurrence for the Lucas-Leonardo \(p\)-numbers · Lucas \(p\)-numbers at indices \(1\) to \(p\) · Recurrence for the Lucas \(p\)-numbers

DefinitionLucas \(p\)-numbers#✓fully proved

For a natural number \(p\), the Lucas \(p\)-numbers are the natural numbers \(L_{p,n}\) given by \(L_{p,0} = p + 1\), \(L_{p,i} = 1\) for \(1 \le i \le p\), and \(L_{p,n} = L_{p,n-1} + L_{p,n-p-1}\) for \(n > p\).

def lucasP (p n : ℕ) : ℕ := (lucasTypeSeq p (p + 1) 0 n).getD n 0

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Section 1 (after (6)).

Uses 1 · Used by 5

Statement usesLucas-type recurrence lists

Used byLucas-Leonardo \(p\)-numbers from Lucas \(p\)-numbers · First values of the Lucas and Lucas-Leonardo \(1\)-numbers · Lucas \(p\)-numbers at indices \(1\) to \(p\) · Recurrence for the Lucas \(p\)-numbers · Initial Lucas \(p\)-number

TheoremInitial Lucas \(p\)-number#✓fully proved

For every natural number \(p\), the Lucas \(p\)-number \(L_{p,0}\) equals \(p + 1\).

theorem lucasP_zero (p : ℕ) : lucasP p 0 = p + 1

Sources

• Belkhir and Tan, INTEGERS 25 (2025), Article A57, Section 1.

Uses 1

Statement usesLucas \(p\)-numbers

TheoremLucas \(p\)-numbers at indices \(1\) to \(p\)#✓fully proved

For every natural number \(p\) and every \(n\) with \(1 \le n \le p\), the Lucas \(p\)-number \(L_{p,n}\) equals \(1\).

theorem lucasP_of_le (p : ℕ) {n : ℕ} (h1 : 1 ≤ n) (hn : n ≤ p) : lucasP p n = 1

Sources

• Belkhir and Tan, INTEGERS 25 (2025), Article A57, Section 1.

Uses 3

Statement usesLucas \(p\)-numbers

Proof usesLucas-type recurrence lists · Last entry of a Lucas-type list

TheoremRecurrence for the Lucas \(p\)-numbers#✓fully proved

For every natural number \(p\), write \(L_{p,n}\) for the Lucas \(p\)-numbers. Then \(L_{p,n} = L_{p,n-1} + L_{p,n-p-1}\) for every \(n > p\).

theorem lucasP_of_lt (p : ℕ) {n : ℕ} (hn : p < n) :
    lucasP p n = lucasP p (n - 1) + lucasP p (n - p - 1)

Sources

• Belkhir and Tan, INTEGERS 25 (2025), Article A57, Section 1.

Uses 3

Statement usesLucas \(p\)-numbers

Proof usesLucas-type recurrence lists · Last entry of a Lucas-type list

DefinitionLucas-Leonardo \(p\)-numbers#✓fully proved

For a natural number \(p\), the Lucas-Leonardo \(p\)-numbers are the integers \(R_{p,n}\) given by \(R_{p,0} = p^2 + p + 1\), \(R_{p,i} = 1\) for \(1 \le i \le p\), and \(R_{p,n} = R_{p,n-1} + R_{p,n-p-1} + p\) for \(n > p\).

def lucasLeonardoP (p n : ℕ) : ℤ :=
  (lucasTypeSeq p ((p : ℤ) ^ 2 + p + 1) (p : ℤ) n).getD n 0

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Section 1, display (5).

Uses 1 · Used by 13

Statement usesLucas-type recurrence lists

Used byCounting Lucas–Leonardo bracelets · Hyper Lucas-Leonardo p-numbers · Hyper Lucas–Leonardo numbers from incomplete ones · Hyper Lucas–Leonardo \(p\)-numbers at \(n = 0\) · Hyper Lucas-Leonardo p-numbers of order zero · Lucas-Leonardo \(p\)-numbers from Leonardo \(p\)-numbers · Lucas-Leonardo \(p\)-numbers from Lucas \(p\)-numbers · Lucas-Leonardo \(p\)-numbers at indices \(1\) to \(p\) · Recurrence for the Lucas-Leonardo \(p\)-numbers · Initial Lucas-Leonardo \(p\)-number · First values of the Lucas and Lucas-Leonardo \(1\)-numbers · Sum of the Lucas-Leonardo p-numbers · Sum of the Lucas-Leonardo p-numbers at multiples of \(p + 1\)

TheoremInitial Lucas-Leonardo \(p\)-number#✓fully proved

For every natural number \(p\), the Lucas-Leonardo \(p\)-number \(R_{p,0}\) equals \(p^2 + p + 1\).

theorem lucasLeonardoP_zero (p : ℕ) : lucasLeonardoP p 0 = (p : ℤ) ^ 2 + p + 1

Sources

• Belkhir and Tan, INTEGERS 25 (2025), Article A57, display (5).

Uses 1

Statement usesLucas-Leonardo \(p\)-numbers

TheoremLucas-Leonardo \(p\)-numbers at indices \(1\) to \(p\)#✓fully proved

For every natural number \(p\) and every \(n\) with \(1 \le n \le p\), the Lucas-Leonardo \(p\)-number \(R_{p,n}\) equals \(1\).

theorem lucasLeonardoP_of_le (p : ℕ) {n : ℕ} (h1 : 1 ≤ n) (hn : n ≤ p) :
    lucasLeonardoP p n = 1

Sources

• Belkhir and Tan, INTEGERS 25 (2025), Article A57, display (5).

Uses 3

Statement usesLucas-Leonardo \(p\)-numbers

Proof usesLucas-type recurrence lists · Last entry of a Lucas-type list

TheoremRecurrence for the Lucas-Leonardo \(p\)-numbers#✓fully proved

For every natural number \(p\), write \(R_{p,n}\) for the Lucas-Leonardo \(p\)-numbers. Then \(R_{p,n} = R_{p,n-1} + R_{p,n-p-1} + p\) for every \(n > p\).

theorem lucasLeonardoP_of_lt (p : ℕ) {n : ℕ} (hn : p < n) :
    lucasLeonardoP p n = lucasLeonardoP p (n - 1) + lucasLeonardoP p (n - p - 1) + p

Sources

• Belkhir and Tan, INTEGERS 25 (2025), Article A57, display (5).

Uses 3

Statement usesLucas-Leonardo \(p\)-numbers

Proof usesLucas-type recurrence lists · Last entry of a Lucas-type list

TheoremFirst values of the Lucas and Lucas-Leonardo \(1\)-numbers#✓fully proved

The Lucas \(1\)-numbers \(L_{1,0}, \dots, L_{1,5}\) are \(2, 1, 3, 4, 7, 11\), and the Lucas-Leonardo \(1\)-numbers \(R_{1,0}, \dots, R_{1,5}\) are \(3, 1, 5, 7, 13, 21\).

theorem lucasP_lucasLeonardoP_one_values :
    (List.range 6).map (lucasP 1) = [2, 1, 3, 4, 7, 11] ∧
      (List.range 6).map (lucasLeonardoP 1) = [3, 1, 5, 7, 13, 21]

Sources

• Belkhir and Tan, INTEGERS 25 (2025), Article A57, Section 1.

Uses 2

Statement usesLucas-Leonardo \(p\)-numbers · Lucas \(p\)-numbers

DefinitionIncomplete Leonardo p-numbers#✓fully proved

For natural numbers \(p\), \(n\) and \(k\), the incomplete Leonardo \(p\)-number is the integer

\[ \mathcal{L}_{p,n}(k) = (p + 1) \sum_{i=0}^{k} \binom{\max(n - pi, 0)}{i} - p. \]

On the paper's range \(0 \le k \le \lfloor n/(p+1) \rfloor\) the maximum is always \(n - pi\).

def incompleteLeonardoP (p n k : ℕ) : ℤ :=
  (p + 1) * ∑ i ∈ Finset.range (k + 1), ((n - p * i).choose i : ℤ) - p

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, display (4).

Used by 5

Used byRecurrence for incomplete Leonardo p-numbers · Incomplete Leonardo p-numbers at zero · Leonardo p-numbers split into incomplete and hyper parts · Binomial sum identity for incomplete Leonardo p-numbers · Partial sums of incomplete Leonardo p-numbers

TheoremIncomplete Leonardo p-numbers at zero#✓fully proved

For all natural numbers \(p\) and \(n\), the incomplete Leonardo \(p\)-number \(\mathcal{L}_{p,n}(0)\) equals \(1\).

theorem incompleteLeonardoP_zero (p n : ℕ) : incompleteLeonardoP p n 0 = 1

Sources

• Belkhir and Tan, INTEGERS 25 (2025), Article A57, display (4).

Uses 1

Statement usesIncomplete Leonardo p-numbers

DefinitionIncomplete Lucas-Leonardo p-numbers#✓fully proved

For natural numbers \(p\), \(n\) and \(k\), the incomplete Lucas-Leonardo \(p\)-number is the rational number

\[ R_{p,n}(k) = (p + 1) \sum_{i=0}^{k} \frac{n}{m_i} \binom{m_i}{i} - p, \qquad m_i = \max(n - pi, 0), \]

where a summand with \(m_i = 0\) is taken to be \(0\). On the paper's range \(0 \le k \le \lfloor n/(p+1) \rfloor\) with \(n \ge 1\), every \(m_i\) is positive.

def incompleteLucasLeonardoP (p n k : ℕ) : ℚ :=
  (p + 1) * ∑ i ∈ Finset.range (k + 1),
    (n : ℚ) / ((n - p * i : ℕ) : ℚ) * ((n - p * i).choose i : ℚ) - p

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, display (8).

Used by 4

Used byHyper Lucas–Leonardo numbers from incomplete ones · Recurrence for incomplete Lucas-Leonardo p-numbers · Incomplete Lucas-Leonardo p-numbers at zero · Binomial sum identity for incomplete Lucas-Leonardo p-numbers

TheoremIncomplete Lucas-Leonardo p-numbers at zero#✓fully proved

For every natural number \(p\) and every natural number \(n \ge 1\), the incomplete Lucas-Leonardo \(p\)-number \(R_{p,n}(0)\) equals \(1\).

theorem incompleteLucasLeonardoP_zero (p n : ℕ) (hn : 1 ≤ n) :
    incompleteLucasLeonardoP p n 0 = 1

Sources

• Belkhir and Tan, INTEGERS 25 (2025), Article A57, display (8).

Uses 1

Statement usesIncomplete Lucas-Leonardo p-numbers

DefinitionHyper Leonardo \(p\)-numbers#✓fully proved

For natural numbers \(p\), \(n\) and \(k\), the hyper Leonardo \(p\)-number is the integer

\[\mathcal{L}^{(k)}_{p,n} = (p + 1) \sum_{i=0}^{\lfloor n/(p+1) \rfloor} \binom{n + k - pi}{i + k} - p \binom{n + k}{k}.\]

def hyperLeonardoP (p n k : ℕ) : ℤ :=
  (p + 1) * ∑ i ∈ Finset.range (n / (p + 1) + 1), ((n + k - p * i).choose (i + k) : ℤ) -
    p * ((n + k).choose k : ℤ)

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, display (12) (quoting Belaggoun and Belbachir).

Used by 5

Used byBinomial addition formula for hyper Leonardo \(p\)-numbers · Recurrence for the hyper Leonardo \(p\)-numbers · Hyper Leonardo \(p\)-numbers at \(n = 0\) · Hyper Lucas–Leonardo numbers from hyper Leonardo numbers · Leonardo p-numbers split into incomplete and hyper parts

TheoremHyper Leonardo \(p\)-numbers at \(n = 0\)#✓fully proved

For all natural numbers \(p\) and \(k\), the hyper Leonardo \(p\)-number \(\mathcal{L}^{(k)}_{p,0}\) equals \(1\).

theorem hyperLeonardoP_zero_left (p k : ℕ) : hyperLeonardoP p 0 k = 1

Sources

• Belkhir and Tan, INTEGERS 25 (2025), Article A57, display (12) and Proposition 10.

Uses 1

Statement usesHyper Leonardo \(p\)-numbers

DefinitionHyper Lucas-Leonardo p-numbers#✓fully proved

For natural numbers \(p\), \(n\) and \(k\), the hyper Lucas-Leonardo \(p\)-number \(R^{(k)}_{p,n}\) is the rational number defined by \(R^{(0)}_{p,n} = R_{p,n}\), the Lucas-Leonardo \(p\)-number; \(R^{(k)}_{p,0} = p^2 + p + 1\) for \(k \ge 1\); and, for \(n \ge 1\) and \(k \ge 1\),

\[ R^{(k)}_{p,n} = (p + 1) \sum_{i=0}^{\lfloor n/(p+1) \rfloor} \frac{n + (p+1)k}{n + k - pi} \binom{n + k - pi}{i + k} - p \binom{n + k}{k}. \]

For \(p = 2\) this reproduces the values listed in the paper. For \(p = 1\) the listed values \(122\) (for \(R^{(1)}_{1,7}\)), \(101, 186, 308\) (for \(R^{(2)}_{1,5}, R^{(2)}_{1,6}, R^{(2)}_{1,7}\)) and \(220, 406, 714\) (for \(R^{(3)}_{1,5}, R^{(3)}_{1,6}, R^{(3)}_{1,7}\)) are misprints: the definition gives \(142\); \(111, 196, 338\); and \(230, 426, 764\), the values that the recurrence \(R^{(k)}_{1,n} = R^{(k)}_{1,n-1} + R^{(k-1)}_{1,n}\) produces from the paper's own earlier entries.

def hyperLucasLeonardoP (p n k : ℕ) : ℚ :=
  if k = 0 then (lucasLeonardoP p n : ℚ)
  else if n = 0 then (p : ℚ) ^ 2 + p + 1
  else (p + 1) * ∑ i ∈ Finset.range (n / (p + 1) + 1),
      ((n + (p + 1) * k : ℕ) : ℚ) / ((n + k - p * i : ℕ) : ℚ) *
        ((n + k - p * i).choose (i + k) : ℚ) -
    p * ((n + k).choose k : ℚ)

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Definition 2.

Uses 1 · Used by 4

Statement usesLucas-Leonardo \(p\)-numbers

Used byHyper Lucas–Leonardo numbers from incomplete ones · Hyper Lucas–Leonardo numbers from hyper Leonardo numbers · Hyper Lucas–Leonardo \(p\)-numbers at \(n = 0\) · Hyper Lucas-Leonardo p-numbers of order zero

TheoremHyper Lucas–Leonardo \(p\)-numbers at \(n = 0\)#✓fully proved

For all natural numbers \(p\) and \(k\), the hyper Lucas–Leonardo \(p\)-number \(R^{(k)}_{p,0}\) equals \(p^2 + p + 1\).

For \(k = 0\) this is the initial value \(R_{p,0} = p^2 + p + 1\) of the Lucas–Leonardo \(p\)-numbers.

theorem hyperLucasLeonardoP_zero_left (p k : ℕ) :
    hyperLucasLeonardoP p 0 k = (p : ℚ) ^ 2 + p + 1

Sources

• Belkhir and Tan, INTEGERS 25 (2025), Article A57, Definition 2.

Uses 2

Statement usesHyper Lucas-Leonardo p-numbers

Proof usesLucas-Leonardo \(p\)-numbers

TheoremHyper Lucas-Leonardo p-numbers of order zero#✓fully proved

For all natural numbers \(p\) and \(n\), the hyper Lucas-Leonardo \(p\)-number of order \(0\) equals the Lucas-Leonardo \(p\)-number: \(R^{(0)}_{p,n} = R_{p,n}\).

theorem hyperLucasLeonardoP_zero_right (p n : ℕ) :
    hyperLucasLeonardoP p n 0 = lucasLeonardoP p n

Sources

• Belkhir and Tan, INTEGERS 25 (2025), Article A57, Definition 2.

Uses 2

Statement usesHyper Lucas-Leonardo p-numbers · Lucas-Leonardo \(p\)-numbers

DefinitionLeonardo \(p\)-tilings#✓fully proved

For natural numbers \(p\) and \(n\), the tiling set \(K_{p,n}\) consists of the linear tilings of an \(n\)-board by squares (length \(1\)), \(p\)-minos (length \(p + 1\)) and at most one \(p\)-tile, which comes in one of \(p\) colors, has length at least \(p + 1\), and can only be the initial piece. A tiling is recorded as its initial \(p\)-tile, given by its color and length, if there is one, followed by the sequence of the remaining pieces read from left to right, each a square or a \(p\)-mino; the lengths of all pieces sum to \(n\).

def leonardoPTilings (p n : ℕ) : Set (Option (Fin p × ℕ) × List Bool) :=
  {t | (∀ c l, t.1 = some (c, l) → p + 1 ≤ l) ∧
    t.1.elim 0 Prod.snd + (t.2.map fun b => if b then p + 1 else 1).sum = n}

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Definition 1 and the set K_{p,n} before Proposition 1.

Used by 2

Used byCounting Leonardo \(p\)-tilings · The all-squares tiling is a Leonardo \(p\)-tiling

TheoremThe all-squares tiling is a Leonardo \(p\)-tiling#✓fully proved

For all natural numbers \(p\) and \(n\), the linear tiling of an \(n\)-board by \(n\) squares, with no \(p\)-tile, lies in the tiling set \(K_{p,n}\).

theorem replicate_mem_leonardoPTilings (p n : ℕ) :
    ((none : Option (Fin p × ℕ)), List.replicate n false) ∈ leonardoPTilings p n

Sources

• Belkhir and Tan, INTEGERS 25 (2025), Article A57, Section 2.

Uses 1

Statement usesLeonardo \(p\)-tilings

InductiveFirst tile of a bracelet#✓fully proved

For a natural number \(p\), a first tile records the tile of a bracelet that covers cell \(1\) of the circular board, together with its phase (which cell of the tile covers cell \(1\)). It is one of: a curved square, in phase \(1\); a curved \(p\)-mino of length \(p + 1\) in phase \(r + 1\) for some \(0 \le r \le p\); a curved \(p\)-tile of length \(p + 1\) in color \(c\) for some \(0 \le c < p\) and phase \(r + 1\) for some \(0 \le r \le p\); or a curved \(p\)-tile of length \(l\) in color \(c\) for some \(0 \le c < p\) and some natural number \(l\), starting at cell \(1\) (phase \(1\)).

The restriction \(l \ge p + 2\) on the last kind is not part of this type; the bracelet sets impose it.

inductive BraceletFirstTile (p : ℕ) where
  /-- A curved square (phase `1`). -/
  | square
  /-- A curved `p`-mino (length `p + 1`) in phase `r + 1`. -/
  | mino (r : Fin (p + 1))
  /-- A curved `p`-tile of length `p + 1`, in color `c` and phase `r + 1`. -/
  | shortTile (c : Fin p) (r : Fin (p + 1))
  /-- A curved `p`-tile of length `l` in color `c`, starting at cell `1` (phase `1`). -/
  | longTile (c : Fin p) (l : ℕ)

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Section 3.

Used by 4

Used byCounting Lucas–Leonardo bracelets · Length of the first tile of a bracelet · Lucas–Leonardo bracelets · The all-squares bracelet is a Lucas–Leonardo bracelet

DefinitionLength of the first tile of a bracelet#✓fully proved

For a natural number \(p\), the length of the first tile of a bracelet is \(1\) for a curved square, \(p + 1\) for a curved \(p\)-mino in any phase, \(p + 1\) for a curved \(p\)-tile of length \(p + 1\) in any color and phase, and \(l\) for a curved \(p\)-tile of length \(l\) (in any color) starting at cell \(1\).

def BraceletFirstTile.length {p : ℕ} : BraceletFirstTile p → ℕ
  | .square => 1
  | .mino _ => p + 1
  | .shortTile _ _ => p + 1
  | .longTile _ l => l

Sources

• Belkhir and Tan, INTEGERS 25 (2025), Article A57, Section 3.

Uses 1 · Used by 1

Statement usesFirst tile of a bracelet

Used byLucas–Leonardo bracelets

DefinitionLucas–Leonardo bracelets#✓fully proved

For natural numbers \(p\) and \(n\), the bracelet set \(B_{p,n}\) consists of the tilings of a circular \(n\)-board by curved squares (length \(1\)), curved \(p\)-minos (length \(p + 1\)) and at most one curved \(p\)-tile, which comes in one of \(p\) colors and has either length \(p + 1\), in any of its \(p + 1\) phases, or length \(l \ge p + 2\), starting at cell \(1\); a \(p\)-tile, if present, is the first tile. A bracelet is recorded as its first tile, the one covering cell \(1\), together with its phase, followed by the sequence of the remaining pieces read clockwise, each a curved square or a curved \(p\)-mino; the lengths of all pieces sum to \(n\). In particular \(B_{p,0}\) is empty.

The source sets \(|B_{p,0}| = p^2 + p + 1\) by convention; that value is not modelled here.

def lucasLeonardoBracelets (p n : ℕ) : Set (BraceletFirstTile p × List Bool) :=
  {b | (∀ c l, b.1 = .longTile c l → p + 2 ≤ l) ∧
    b.1.length + (b.2.map fun t => if t then p + 1 else 1).sum = n}

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Section 3, the set B_{p,n} before Proposition 12.

Uses 2 · Used by 2

Statement usesFirst tile of a bracelet · Length of the first tile of a bracelet

Used byCounting Lucas–Leonardo bracelets · The all-squares bracelet is a Lucas–Leonardo bracelet

TheoremThe all-squares bracelet is a Lucas–Leonardo bracelet#✓fully proved

For every natural number \(p\) and every natural number \(n \ge 1\), the bracelet whose first tile is a curved square covering cell \(1\) and whose remaining \(n - 1\) pieces are all curved squares lies in the bracelet set \(B_{p,n}\).

theorem square_replicate_mem_lucasLeonardoBracelets (p n : ℕ) (hn : 1 ≤ n) :
    ((.square : BraceletFirstTile p), List.replicate (n - 1) false) ∈
      lucasLeonardoBracelets p n

Sources

• Belkhir and Tan, INTEGERS 25 (2025), Article A57, Section 3.

Uses 2

Statement usesFirst tile of a bracelet · Lucas–Leonardo bracelets

TheoremCounting Leonardo \(p\)-tilings#●ready to prove

For all natural numbers \(p \ge 1\) and \(n\), let \(K_{p,n}\) be the set of linear tilings of an \(n\)-board by squares (length \(1\)), \(p\)-minos (length \(p + 1\)) and at most one \(p\)-tile, which comes in one of \(p\) colors, has length at least \(p + 1\) and can only be the initial piece. Then the number of tilings in \(K_{p,n}\) equals the Leonardo \(p\)-number \(\mathcal{L}_{p,n}\), the generalized Leonardo \(p\)-number \(\mathcal{L}_{p,k}(n)\) at \(k = p\): \(\mathcal{L}_{p,n} = 1\) for \(n \le p\) and \(\mathcal{L}_{p,n} = \mathcal{L}_{p,n-1} + \mathcal{L}_{p,n-p-1} + p\) for \(n > p\).

public theorem_wanted card_leonardoPTilings (p n : ℕ) (hp : 1 ≤ p) :
    (Nat.card (leonardoPTilings p n) : ℤ) = leonardoPK p p n

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Proposition 1.

Uses 2

Statement usesGeneralized Leonardo \(p\)-numbers · Leonardo \(p\)-tilings

TheoremHomogeneous recurrence for the Leonardo \(p\)-numbers#●ready to prove

Let \(p \ge 1\) and write \(\mathcal{L}_{p,n}\) for the Leonardo \(p\)-number \(\mathcal{L}_{p,p}(n)\), the generalized Leonardo \(p\)-number with \(k = p\). Then \(\mathcal{L}_{p,n} = \mathcal{L}_{p,n-1} + \mathcal{L}_{p,n-p} - \mathcal{L}_{p,n-2p-1}\) for every \(n \ge 2p + 1\), \(\mathcal{L}_{p,i} = 1\) for every \(i \le p\), and \(\mathcal{L}_{p,p+j} = (j + 1) + jp\) for every \(j\) with \(1 \le j \le p\).

public theorem_wanted leonardoPK_self_homogeneous (p : ℕ) (hp : 1 ≤ p) :
    (∀ n, 2 * p + 1 ≤ n →
      leonardoPK p p n =
        leonardoPK p p (n - 1) + leonardoPK p p (n - p) - leonardoPK p p (n - 2 * p - 1)) ∧
    (∀ i, i ≤ p → leonardoPK p p i = 1) ∧
    (∀ j, 1 ≤ j → j ≤ p → leonardoPK p p (p + j) = (j : ℤ) + 1 + j * p)

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Proposition 2.

Uses 1

Statement usesGeneralized Leonardo \(p\)-numbers

TheoremRecurrence for incomplete Leonardo p-numbers#●ready to prove

For natural numbers \(p \ge 1\), \(n > p\) and \(k \le \lfloor n/(p+1) \rfloor\), the incomplete Leonardo \(p\)-numbers \(\mathcal{L}_{p,m}(j)\) satisfy

\[ \mathcal{L}_{p,n}(k + 1) = \mathcal{L}_{p,n-1}(k + 1) + \mathcal{L}_{p,n-p-1}(k) + p. \]

public theorem_wanted incompleteLeonardoP_succ (p n k : ℕ) (hp : 1 ≤ p) (hn : p < n)
    (hk : k ≤ n / (p + 1)) :
    incompleteLeonardoP p n (k + 1) =
      incompleteLeonardoP p (n - 1) (k + 1) + incompleteLeonardoP p (n - p - 1) k + p

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Proposition 6.

Uses 1

Statement usesIncomplete Leonardo p-numbers

TheoremBinomial sum identity for incomplete Leonardo p-numbers#●ready to prove

For natural numbers \(p \ge 1\), \(n\), \(r\) and \(k\) with \(n \ge p + r\) and \(k \le \lfloor (n - p - r)/(p + 1) \rfloor\), the incomplete Leonardo \(p\)-numbers \(\mathcal{L}_{p,m}(j)\) satisfy

\[ \sum_{i=0}^{r} \binom{r}{i} \mathcal{L}_{p,n+pi}(k + i) + (2^r - 1) p = \mathcal{L}_{p,n+(p+1)r}(k + r). \]

public theorem_wanted sum_choose_mul_incompleteLeonardoP (p n r k : ℕ) (hp : 1 ≤ p)
    (hnr : p + r ≤ n) (hk : k ≤ (n - p - r) / (p + 1)) :
    ∑ i ∈ Finset.range (r + 1), (r.choose i : ℤ) * incompleteLeonardoP p (n + p * i) (k + i) +
        ((2 : ℤ) ^ r - 1) * p =
      incompleteLeonardoP p (n + (p + 1) * r) (k + r)

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Proposition 7.

Uses 1

Statement usesIncomplete Leonardo p-numbers

TheoremPartial sums of incomplete Leonardo p-numbers#●ready to prove

For natural numbers \(p \ge 1\), \(n\), \(k\) and \(r\) with \(n \ge (p + 1)(k + 1)\), the incomplete Leonardo \(p\)-numbers \(\mathcal{L}_{p,m}(j)\) satisfy

\[ \sum_{i=0}^{r-1} \mathcal{L}_{p,n-p+i}(k) + rp = \mathcal{L}_{p,n+r}(k + 1) - \mathcal{L}_{p,n}(k + 1), \]

where the sum is empty when \(r = 0\).

public theorem_wanted sum_incompleteLeonardoP (p n k r : ℕ) (hp : 1 ≤ p)
    (hn : (p + 1) * (k + 1) ≤ n) :
    ∑ i ∈ Finset.range r, incompleteLeonardoP p (n - p + i) k + (r : ℤ) * p =
      incompleteLeonardoP p (n + r) (k + 1) - incompleteLeonardoP p n (k + 1)

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Proposition 8.

Uses 1

Statement usesIncomplete Leonardo p-numbers

TheoremBinomial addition formula for hyper Leonardo \(p\)-numbers#●ready to prove

For natural numbers \(p \ge 1\), \(n \ge 1\), \(m \ge 1\) and \(k \ge m\), the hyper Leonardo \(p\)-numbers satisfy

\[\mathcal{L}^{(k)}_{p,n+m} = \sum_{i=0}^{m} \binom{m}{i} \mathcal{L}^{(k-i)}_{p,n+i}.\]

public theorem_wanted hyperLeonardoP_add (p n m k : ℕ) (hp : 1 ≤ p) (hn : 1 ≤ n)
    (hm : 1 ≤ m) (hmk : m ≤ k) :
    hyperLeonardoP p (n + m) k =
      ∑ i ∈ Finset.range (m + 1), (m.choose i : ℤ) * hyperLeonardoP p (n + i) (k - i)

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Proposition 9.

Uses 1

Statement usesHyper Leonardo \(p\)-numbers

TheoremRecurrence for the hyper Leonardo \(p\)-numbers#●ready to prove

Let \(p \ge 1\) be a natural number. For all natural numbers \(n \ge 1\) and \(k \ge 1\), the hyper Leonardo \(p\)-numbers satisfy \(\mathcal{L}^{(k)}_{p,n} = \mathcal{L}^{(k)}_{p,n-1} + \mathcal{L}^{(k-1)}_{p,n}\), and for every natural number \(n\), \(\mathcal{L}^{(0)}_{p,n} = \mathcal{L}_{p,n}\), where \(\mathcal{L}_{p,n}\) is the Leonardo \(p\)-number: \(\mathcal{L}_{p,n} = 1\) for \(n \le p\) and \(\mathcal{L}_{p,n} = \mathcal{L}_{p,n-1} + \mathcal{L}_{p,n-p-1} + p\) for \(n > p\).

public theorem_wanted hyperLeonardoP_rec (p : ℕ) (hp : 1 ≤ p) :
    (∀ n k, 1 ≤ n → 1 ≤ k →
      hyperLeonardoP p n k = hyperLeonardoP p (n - 1) k + hyperLeonardoP p n (k - 1)) ∧
    ∀ n, hyperLeonardoP p n 0 = leonardoPK p p n

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Proposition 10.

Uses 2

Statement usesGeneralized Leonardo \(p\)-numbers · Hyper Leonardo \(p\)-numbers

TheoremLeonardo p-numbers split into incomplete and hyper parts#●ready to prove

For natural numbers \(p \ge 1\), \(n > p\) and \(k \ge 1\), let \(N = n + (p + 1)k\). Then

\[ \mathcal{L}_{p,N} = \mathcal{L}_{p,N}(k - 1) + \mathcal{L}^{(k)}_{p,n} + p \binom{n + k}{k}, \]

where \(\mathcal{L}_{p,N}\) is the Leonardo \(p\)-number (the generalized Leonardo \(p\)-numbers with additive constant \(p\): \(\mathcal{L}_{p,m} = 1\) for \(m \le p\) and \(\mathcal{L}_{p,m} = \mathcal{L}_{p,m-1} + \mathcal{L}_{p,m-p-1} + p\) for \(m > p\)), \(\mathcal{L}_{p,N}(k - 1)\) is the incomplete Leonardo \(p\)-number and \(\mathcal{L}^{(k)}_{p,n}\) is the hyper Leonardo \(p\)-number.

public theorem_wanted leonardoPK_eq_incomplete_add_hyper (p n k : ℕ) (hp : 1 ≤ p)
    (hn : p < n) (hk : 1 ≤ k) :
    leonardoPK p p (n + (p + 1) * k) =
      incompleteLeonardoP p (n + (p + 1) * k) (k - 1) + hyperLeonardoP p n k +
        p * ((n + k).choose k : ℤ)

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Proposition 11.

Uses 3

Statement usesGeneralized Leonardo \(p\)-numbers · Hyper Leonardo \(p\)-numbers · Incomplete Leonardo p-numbers

TheoremCounting Lucas–Leonardo bracelets#●ready to prove

For all natural numbers \(p \ge 1\) and \(n \ge 1\), let \(B_{p,n}\) be the set of tilings of a circular \(n\)-board by curved squares (length \(1\)), curved \(p\)-minos (length \(p + 1\)) and at most one curved \(p\)-tile in one of \(p\) colors, which if present is the tile covering cell \(1\) and either has length \(p + 1\), in any of its \(p + 1\) phases, or has length at least \(p + 2\) and starts at cell \(1\). Then the number of bracelets in \(B_{p,n}\) equals the Lucas–Leonardo \(p\)-number \(R_{p,n}\), given by \(R_{p,0} = p^2 + p + 1\), \(R_{p,i} = 1\) for \(1 \le i \le p\) and \(R_{p,n} = R_{p,n-1} + R_{p,n-p-1} + p\) for \(n > p\).

public theorem_wanted card_lucasLeonardoBracelets (p n : ℕ) (hp : 1 ≤ p) (hn : 1 ≤ n) :
    (Nat.card (lucasLeonardoBracelets p n) : ℤ) = lucasLeonardoP p n

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Proposition 12.

Uses 3

Statement usesFirst tile of a bracelet · Lucas–Leonardo bracelets · Lucas-Leonardo \(p\)-numbers

TheoremLucas-Leonardo \(p\)-numbers from Lucas \(p\)-numbers#●ready to prove

For every \(p \ge 1\) and every natural number \(n\), the Lucas-Leonardo \(p\)-number \(R_{p,n}\) and the Lucas \(p\)-number \(L_{p,n}\) satisfy \(R_{p,n} = (p + 1) L_{p,n} - p\).

public theorem_wanted lucasLeonardoP_eq_lucasP (p n : ℕ) (hp : 1 ≤ p) :
    lucasLeonardoP p n = ((p : ℤ) + 1) * lucasP p n - p

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Proposition 13.

Uses 2

Statement usesLucas-Leonardo \(p\)-numbers · Lucas \(p\)-numbers

TheoremLucas-Leonardo \(p\)-numbers from Leonardo \(p\)-numbers#●ready to prove

Let \(p \ge 1\), let \(R_{p,n}\) denote the Lucas-Leonardo \(p\)-numbers, and let \(\mathcal{L}_{p,n}\) denote the Leonardo \(p\)-numbers \(\mathcal{L}_{p,p}(n)\) (the generalized Leonardo \(p\)-numbers with \(k = p\)), extended to \(n = -1\) by \(\mathcal{L}_{p,-1} = -p\). Then \(R_{p,n} = (p + 1) \mathcal{L}_{p,n} - p \mathcal{L}_{p,n-1}\) for every natural number \(n\).

public theorem_wanted lucasLeonardoP_eq_leonardoPK (p n : ℕ) (hp : 1 ≤ p) :
    lucasLeonardoP p n = ((p : ℤ) + 1) * leonardoPK p p n - p * leonardoPKZ p p ((n : ℤ) - 1)

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Proposition 14.

Uses 3

Statement usesGeneralized Leonardo \(p\)-numbers · Generalized Leonardo \(p\)-numbers at integer arguments · Lucas-Leonardo \(p\)-numbers

TheoremSum of the Lucas-Leonardo p-numbers#●ready to prove

For every natural number \(p \ge 1\) and every natural number \(n\), the Lucas-Leonardo \(p\)-numbers \(R_{p,m}\) satisfy \(\sum_{i=0}^{n} R_{p,i} = R_{p,n+p+1} - p(n + 1) - 1\).

public theorem_wanted sum_lucasLeonardoP (p n : ℕ) (hp : 1 ≤ p) :
    ∑ i ∈ Finset.range (n + 1), lucasLeonardoP p i =
      lucasLeonardoP p (n + p + 1) - p * ((n : ℤ) + 1) - 1

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Proposition 15.

Uses 1

Statement usesLucas-Leonardo \(p\)-numbers

TheoremSum of the Lucas-Leonardo p-numbers at multiples of \(p + 1\)#●ready to prove

For every natural number \(p \ge 1\) and every natural number \(n\), the Lucas-Leonardo \(p\)-numbers \(R_{p,m}\) satisfy \(\sum_{i=0}^{n} R_{p,(p+1)i} = R_{p,(p+1)n+1} - p(n - p - 1)\), an identity of integers.

public theorem_wanted sum_lucasLeonardoP_stride (p n : ℕ) (hp : 1 ≤ p) :
    ∑ i ∈ Finset.range (n + 1), lucasLeonardoP p ((p + 1) * i) =
      lucasLeonardoP p ((p + 1) * n + 1) - p * ((n : ℤ) - p - 1)

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Proposition 16.

Uses 1

Statement usesLucas-Leonardo \(p\)-numbers

TheoremRecurrence for incomplete Lucas-Leonardo p-numbers#●ready to prove

For natural numbers \(p \ge 1\), \(n > p + 1\) and \(k \le \lfloor n/(p+1) \rfloor\), the incomplete Lucas-Leonardo \(p\)-numbers \(R_{p,m}(j)\) satisfy

\[ R_{p,n}(k + 1) = R_{p,n-1}(k + 1) + R_{p,n-p-1}(k) + p. \]

At \(n = p + 1\) the term \(R_{p,0}(k)\) would contain the undefined summand \(\frac{0}{0} \binom{0}{0}\), so that case is excluded.

public theorem_wanted incompleteLucasLeonardoP_succ (p n k : ℕ) (hp : 1 ≤ p)
    (hn : p + 1 < n) (hk : k ≤ n / (p + 1)) :
    incompleteLucasLeonardoP p n (k + 1) =
      incompleteLucasLeonardoP p (n - 1) (k + 1) + incompleteLucasLeonardoP p (n - p - 1) k +
        p

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Proposition 17.

Uses 1

Statement usesIncomplete Lucas-Leonardo p-numbers

TheoremBinomial sum identity for incomplete Lucas-Leonardo p-numbers#●ready to prove

For natural numbers \(p \ge 1\), \(n\), \(r\) and \(k\) with \(n \ge p + r\) and \(k \le \lfloor (n - p - r)/(p + 1) \rfloor\), the incomplete Lucas-Leonardo \(p\)-numbers \(R_{p,m}(j)\) satisfy, as rational numbers,

\[ \sum_{i=0}^{r} \binom{r}{i} R_{p,n+pi}(k + i) + (2^r - 1) p = R_{p,n+(p+1)r}(k + r). \]

The paper prints the range as \(0 \le n \le \lfloor (n - p - r)/(p + 1) \rfloor\); the first \(n\) is read as \(k\), as in Proposition 7.

public theorem_wanted sum_choose_mul_incompleteLucasLeonardoP (p n r k : ℕ) (hp : 1 ≤ p)
    (hnr : p + r ≤ n) (hk : k ≤ (n - p - r) / (p + 1)) :
    ∑ i ∈ Finset.range (r + 1),
        (r.choose i : ℚ) * incompleteLucasLeonardoP p (n + p * i) (k + i) +
        ((2 : ℚ) ^ r - 1) * p =
      incompleteLucasLeonardoP p (n + (p + 1) * r) (k + r)

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Proposition 18.

Uses 1

Statement usesIncomplete Lucas-Leonardo p-numbers

TheoremHyper Lucas–Leonardo numbers from incomplete ones#●ready to prove

For natural numbers \(p \ge 1\), \(n > p\) and \(k \ge 1\), write \(R_{p,m}\) for the Lucas–Leonardo \(p\)-numbers and \(R_{p,m}(j)\) for the incomplete Lucas–Leonardo \(p\)-numbers. Then the hyper Lucas–Leonardo \(p\)-number \(R^{(k)}_{p,n}\) satisfies

\[R^{(k)}_{p,n} = R_{p,n+(p+1)k} - R_{p,n+(p+1)k}(k - 1) - p \binom{n + k}{k}.\]

public theorem_wanted hyperLucasLeonardoP_eq (p n k : ℕ) (hp : 1 ≤ p) (hn : p < n)
    (hk : 1 ≤ k) :
    hyperLucasLeonardoP p n k =
      lucasLeonardoP p (n + (p + 1) * k) -
        incompleteLucasLeonardoP p (n + (p + 1) * k) (k - 1) - p * ((n + k).choose k : ℚ)

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Proposition 19.

Uses 3

Statement usesHyper Lucas-Leonardo p-numbers · Incomplete Lucas-Leonardo p-numbers · Lucas-Leonardo \(p\)-numbers

TheoremHyper Lucas–Leonardo numbers from hyper Leonardo numbers#●ready to prove

For natural numbers \(p \ge 1\), \(n > p\) and \(k \ge 1\), the hyper Lucas–Leonardo \(p\)-number \(R^{(k)}_{p,n}\) and the hyper Leonardo \(p\)-numbers \(\mathcal{L}^{(k)}_{p,n}\) satisfy

\[R^{(k)}_{p,n} = (p + 1) \mathcal{L}^{(k)}_{p,n} - p \mathcal{L}^{(k)}_{p,n-1} + p^2 \binom{n + k - 1}{k - 1}.\]

The paper prints the binomial as \(\binom{n + k - 1}{k}\), which is false: at \(p = 1\), \(n = 2\), \(k = 1\) one has \(R^{(1)}_{1,2} = 9\) while the printed right side is \(10\). The paper's own proof ends with \(p^2 \binom{n + k - 1}{k - 1}\).

public theorem_wanted hyperLucasLeonardoP_eq_hyperLeonardoP (p n k : ℕ) (hp : 1 ≤ p)
    (hn : p < n) (hk : 1 ≤ k) :
    hyperLucasLeonardoP p n k =
      ((p : ℚ) + 1) * hyperLeonardoP p n k - p * hyperLeonardoP p (n - 1) k +
        (p : ℚ) ^ 2 * ((n + k - 1).choose (k - 1) : ℚ)

Sources

• Amine Belkhir and Elif Tan, Combinatorial Insights into Leonardo p-Numbers and Lucas-Leonardo p-Numbers, INTEGERS 25 (2025), Article A57, Proposition 20.

Uses 2

Statement usesHyper Leonardo \(p\)-numbers · Hyper Lucas-Leonardo p-numbers

DefinitionSupergeneralized Leonardo p-numbers#✓fully proved

For natural numbers \(p\) and \(k\) and a real sequence \(x = (x_n)_{n \in \mathbb{N}}\), the supergeneralized Leonardo \(p\)-numbers are the real numbers \(\mathcal{L}_{p,k,x}(n)\), \(n \in \mathbb{N}\), given by \(\mathcal{L}_{p,k,x}(n) = x_n\) for \(n \le p\) and \(\mathcal{L}_{p,k,x}(n) = \mathcal{L}_{p,k,x}(n-1) + \mathcal{L}_{p,k,x}(n-p-1) + k\) for \(n > p\). Only the initial values \(x_0, \dots, x_p\) are used.

noncomputable def superLeonardoP (p k : ℕ) (x : ℕ → ℝ) (n : ℕ) : ℝ :=
  if _h : n ≤ p then x n
  else superLeonardoP p k x (n - 1) + superLeonardoP p k x (n - p - 1) + k
termination_by n
decreasing_by all_goals omega

Sources

• Clemens Schütz and Kristian Kelly, An Explicit Formula for Supergeneralized Leonardo p-numbers, Journal of Integer Sequences 28 (2025), Article 25.8.2, Definition 1.

Used by 7

Used byReduction of supergeneralized Leonardo p-numbers to the homogeneous case · Supergeneralized Leonardo p-numbers via Fibonacci p-numbers · Explicit formula for the supergeneralized Leonardo p-numbers · Initial values of the supergeneralized Leonardo p-numbers · Recurrence for the supergeneralized Leonardo p-numbers · Binomial sum for supergeneralized Leonardo p-numbers with linear initial values · Homogeneous supergeneralized Leonardo p-numbers via Fibonacci p-numbers

TheoremInitial values of the supergeneralized Leonardo p-numbers#✓fully proved

For all natural numbers \(p\), \(k\) and \(n\) with \(n \le p\) and every real sequence \(x\), the supergeneralized Leonardo \(p\)-number \(\mathcal{L}_{p,k,x}(n)\) equals \(x_n\).

theorem superLeonardoP_of_le (p k : ℕ) (x : ℕ → ℝ) {n : ℕ} (hn : n ≤ p) :
    superLeonardoP p k x n = x n

Sources

• Schütz and Kelly, Journal of Integer Sequences 28 (2025), Article 25.8.2, Definition 1.

Uses 1

Statement usesSupergeneralized Leonardo p-numbers

TheoremRecurrence for the supergeneralized Leonardo p-numbers#✓fully proved

For all natural numbers \(p\), \(k\) and \(n\) with \(n > p\) and every real sequence \(x\), the supergeneralized Leonardo \(p\)-numbers \(\mathcal{L}_{p,k,x}\) satisfy \(\mathcal{L}_{p,k,x}(n) = \mathcal{L}_{p,k,x}(n-1) + \mathcal{L}_{p,k,x}(n-p-1) + k\).

theorem superLeonardoP_of_lt (p k : ℕ) (x : ℕ → ℝ) {n : ℕ} (hn : p < n) :
    superLeonardoP p k x n =
      superLeonardoP p k x (n - 1) + superLeonardoP p k x (n - p - 1) + k

Sources

• Schütz and Kelly, Journal of Integer Sequences 28 (2025), Article 25.8.2, Definition 1.

Uses 1

Statement usesSupergeneralized Leonardo p-numbers

TheoremReduction of supergeneralized Leonardo p-numbers to the homogeneous case#●ready to prove

Let \(p \ge 1\) and \(k\) be natural numbers, \(x\) a real sequence, \(y\) the real sequence \(y_i = i + 1\), and write \(\mathcal{L}_{p,k,x}(n)\) for the supergeneralized Leonardo \(p\)-numbers. For every natural number \(n\), \(\mathcal{L}_{p,k,x}(n) = \mathcal{L}_{p,0,x}(n)\) if \(n \le p\), and \(\mathcal{L}_{p,k,x}(n) = \mathcal{L}_{p,0,x}(n) + \mathcal{L}_{p,1,y}(n-(p+1)) \cdot k\) if \(n > p\).

The paper writes the correction term as \(\max\{0, \mathcal{L}_{p,1,y}(n-(p+1))\} \cdot k\) with \(y = (1, \dots, p + 1)\) and sets \(\mathcal{L} \le 0\) at negative indices, so the correction term is \(0\) for \(n \le p\); for \(n > p\) the \(\max\) is redundant since \(\mathcal{L}_{p,1,y}\) is positive.

public theorem_wanted superLeonardoP_eq_add_mul (p k : ℕ) (hp : 1 ≤ p) (x : ℕ → ℝ) (n : ℕ) :
    superLeonardoP p k x n =
      superLeonardoP p 0 x n +
        (if p < n then superLeonardoP p 1 (fun i => (i : ℝ) + 1) (n - (p + 1)) else 0) *
          k

Sources

• Clemens Schütz and Kristian Kelly, An Explicit Formula for Supergeneralized Leonardo p-numbers, Journal of Integer Sequences 28 (2025), Article 25.8.2, Theorem 3.

Uses 1

Statement usesSupergeneralized Leonardo p-numbers

TheoremHomogeneous supergeneralized Leonardo p-numbers via Fibonacci p-numbers#●ready to prove

For all natural numbers \(p \ge 1\) and \(n\) and every real sequence \(x\), the supergeneralized Leonardo \(p\)-numbers \(\mathcal{L}_{p,0,x}\) with \(k = 0\) satisfy \(\mathcal{L}_{p,0,x}(n) = x_n\) if \(n \le p\), and if \(n > p\), with \(F_p\) denoting the Fibonacci \(p\)-numbers,

\[\mathcal{L}_{p,0,x}(n) = F_p(n-p+1)\,x_p + \sum_{i=0}^{\min(p-1,\,n-p-1)} F_p(n-p-i)\,x_i.\]

public theorem_wanted superLeonardoP_zero_eq (p : ℕ) (hp : 1 ≤ p) (x : ℕ → ℝ) (n : ℕ) :
    superLeonardoP p 0 x n =
      if n ≤ p then x n
      else (fibonacciP p (n - p + 1) : ℝ) * x p +
        ∑ i ∈ Finset.range (min (p - 1) (n - p - 1) + 1),
          (fibonacciP p (n - p - i) : ℝ) * x i

Sources

• Clemens Schütz and Kristian Kelly, An Explicit Formula for Supergeneralized Leonardo p-numbers, Journal of Integer Sequences 28 (2025), Article 25.8.2, Theorem 4.

Uses 2

Statement usesFibonacci p-numbers · Supergeneralized Leonardo p-numbers

TheoremBinomial sum for supergeneralized Leonardo p-numbers with linear initial values#●ready to prove

Let \(p \ge 1\) be a natural number and \(y\) the real sequence \(y_i = i + 1\), so that the initial values are \(y_0, \dots, y_p = 1, \dots, p + 1\). For every natural number \(n\), the supergeneralized Leonardo \(p\)-numbers \(\mathcal{L}_{p,1,y}\) with \(k = 1\) and initial values \(y\) satisfy

\[\mathcal{L}_{p,1,y}(n) = \sum_{i=0}^{\lfloor (n+1)/(p+1) \rfloor} \binom{n+1-pi}{i+1}.\]

public theorem_wanted superLeonardoP_one_succ_eq_sum_choose (p : ℕ) (hp : 1 ≤ p) (n : ℕ) :
    superLeonardoP p 1 (fun i => (i : ℝ) + 1) n =
      ∑ i ∈ Finset.range ((n + 1) / (p + 1) + 1), ((n + 1 - p * i).choose (i + 1) : ℝ)

Sources

• Clemens Schütz and Kristian Kelly, An Explicit Formula for Supergeneralized Leonardo p-numbers, Journal of Integer Sequences 28 (2025), Article 25.8.2, Theorem 5.

Uses 1

Statement usesSupergeneralized Leonardo p-numbers

TheoremSchütz–Kelly binomial sum identity#●ready to prove

For all natural numbers \(J\), \(n\) and \(p\),

\[1 + \sum_{i=0}^{J} \binom{\max(n-pi,\,0)}{i+1} + \sum_{i=0}^{J-1} \binom{\max(n-pi-p,\,0)}{i+1} = \sum_{i=0}^{J} \binom{\max(n-pi,\,0)+1}{i+1}.\]

Truncating the upper indices at \(0\) makes a negative upper index give \(\binom{0}{i+1} = 0\), matching the paper's binomials. The identity is stated for all natural \(J\), \(n\), \(p\), which includes the value \(0\) beyond the paper's positive range.

public theorem_wanted one_add_sum_choose_add_sum_choose (J n p : ℕ) :
    1 + (∑ i ∈ Finset.range (J + 1), (n - p * i).choose (i + 1)) +
        ∑ i ∈ Finset.range J, (n - p * i - p).choose (i + 1) =
      ∑ i ∈ Finset.range (J + 1), (n - p * i + 1).choose (i + 1)

Sources

• Clemens Schütz and Kristian Kelly, An Explicit Formula for Supergeneralized Leonardo p-numbers, Journal of Integer Sequences 28 (2025), Article 25.8.2, Lemma 6.

TheoremSupergeneralized Leonardo p-numbers via Fibonacci p-numbers#●ready to prove

For all natural numbers \(p \ge 1\), \(k\) and \(n\) with \(n > p\) and every real sequence \(x\), the supergeneralized Leonardo \(p\)-numbers \(\mathcal{L}_{p,k,x}\) and the Fibonacci \(p\)-numbers \(F_p\) satisfy

\[\mathcal{L}_{p,k,x}(n) = F_p(n-p+1)\,x_p + \sum_{i=0}^{\min(p-1,\,n-p-1)} F_p(n-p-i)\,x_i + \max\Big\{0, \sum_{j=0}^{\lfloor (n-p)/(p+1) \rfloor} \binom{n-p-pj}{j+1}\Big\} \cdot k.\]

This is Corollary 7 of the paper with the factor \(k\) restored. The printed corollary omits the factor \(k\) on the last term (and reuses \(k\) as the summation index); without it the identity fails, e.g. at \(p = 1\), \(k = 2\), \(n = 2\), \(x = (1, 1)\): \(\mathcal{L}_{p,k,x}(n) = 4\) but the printed right side is \(3\). The factor is the one in Theorem 3, of which the corollary is stated to be an immediate combination with Theorems 4 and 5.

public theorem_wanted superLeonardoP_eq_fibonacciP_sum (p k : ℕ) (hp : 1 ≤ p) (x : ℕ → ℝ) (n : ℕ)
    (hn : p < n) :
    superLeonardoP p k x n =
      (fibonacciP p (n - p + 1) : ℝ) * x p +
        (∑ i ∈ Finset.range (min (p - 1) (n - p - 1) + 1),
          (fibonacciP p (n - p - i) : ℝ) * x i) +
        max 0 (∑ j ∈ Finset.range ((n - p) / (p + 1) + 1),
          ((n - p - p * j).choose (j + 1) : ℝ)) * k

Sources

• Clemens Schütz and Kristian Kelly, An Explicit Formula for Supergeneralized Leonardo p-numbers, Journal of Integer Sequences 28 (2025), Article 25.8.2, Corollary 7.

Uses 2

Statement usesFibonacci p-numbers · Supergeneralized Leonardo p-numbers

TheoremBinomial sum formula for Fibonacci p-numbers#●ready to prove

For all natural numbers \(p \ge 1\) and \(n\), the Fibonacci \(p\)-numbers \(F_p\) satisfy

\[F_p(n+1) = \sum_{i=0}^{\lfloor n/(p+1) \rfloor} \binom{n-ip}{i}.\]

The paper (Theorem 8, quoting Kuhapatanakul) also gives the form \(F_p(n) = \sum_{i=0}^{\lfloor (n-1)/(p+1) \rfloor} \binom{n-1-ip}{i}\), which is the same identity with \(n\) shifted by one. The paper allows all natural \(p\), but at \(p = 0\) the sequence is identically zero (\(F_0(1) = F_0(0) + F_0(0) = 0\)) while the sum at \(n = 0\) is \(\binom{0}{0} = 1\), so \(p \ge 1\) is assumed.

public theorem_wanted fibonacciP_succ_eq_sum_choose (p n : ℕ) (hp : 1 ≤ p) :
    fibonacciP p (n + 1) = ∑ i ∈ Finset.range (n / (p + 1) + 1), (n - i * p).choose i

Sources

• Clemens Schütz and Kristian Kelly, An Explicit Formula for Supergeneralized Leonardo p-numbers, Journal of Integer Sequences 28 (2025), Article 25.8.2, Theorem 8 (Kuhapatanakul).

Uses 1

Statement usesFibonacci p-numbers

TheoremExplicit formula for the supergeneralized Leonardo p-numbers#●ready to prove

For all natural numbers \(p \ge 1\), \(k\) and \(n\) with \(n > p\) and every real sequence \(x\), the supergeneralized Leonardo \(p\)-numbers \(\mathcal{L}_{p,k,x}\) satisfy

\[\mathcal{L}_{p,k,x}(n) = \Big(\sum_{i=0}^{\lfloor (n-p)/(p+1) \rfloor} \binom{n-p-ip}{i}\Big) x_p + \sum_{i=0}^{\min(p-1,\,n-p-1)} \Big(\sum_{j=0}^{\lfloor (n-p-i-1)/(p+1) \rfloor} \binom{n-p-i-1-jp}{j}\Big) x_i + \max\Big\{0, \sum_{j=0}^{\lfloor (n-p)/(p+1) \rfloor} \binom{n-p-pj}{j+1}\Big\} \cdot k.\]

This is Theorem 9 of the paper with the factor \(k\) restored: as in Corollary 7, the printed theorem omits the factor \(k\) on the last term and is false without it (same counterexample: \(p = 1\), \(k = 2\), \(n = 2\), \(x = (1, 1)\) gives \(4\) versus \(3\)).

public theorem_wanted superLeonardoP_eq_sum_choose (p k : ℕ) (hp : 1 ≤ p) (x : ℕ → ℝ) (n : ℕ)
    (hn : p < n) :
    superLeonardoP p k x n =
      (∑ i ∈ Finset.range ((n - p) / (p + 1) + 1), ((n - p - i * p).choose i : ℝ)) * x p +
        (∑ i ∈ Finset.range (min (p - 1) (n - p - 1) + 1),
          (∑ j ∈ Finset.range ((n - p - i - 1) / (p + 1) + 1),
            ((n - p - i - 1 - j * p).choose j : ℝ)) * x i) +
        max 0 (∑ j ∈ Finset.range ((n - p) / (p + 1) + 1),
          ((n - p - p * j).choose (j + 1) : ℝ)) * k

Sources

• Clemens Schütz and Kristian Kelly, An Explicit Formula for Supergeneralized Leonardo p-numbers, Journal of Integer Sequences 28 (2025), Article 25.8.2, Theorem 9.

Uses 1

Statement usesSupergeneralized Leonardo p-numbers

42 fully proved37 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.