Integer values of recurrence generating functions

DefinitionGibonacci generating function#✓fully proved

For integers \(a\) and \(b\) and a rational number \(x\), the value of the Gibonacci generating function at \(x\) is the rational number

\[G^{(a,b)}(x) = \frac{(b - a)x + a}{1 - x - x^2}.\]

It is the generating function of the Gibonacci sequence \((G_n)_{n \ge 0}\) with \(G_0 = a\), \(G_1 = b\) and \(G_{n+2} = G_{n+1} + G_n\).

public def gibonacciGeneratingValue (a b : ℤ) (x : ℚ) : ℚ :=
  (((b : ℚ) - (a : ℚ)) * x + (a : ℚ)) / (1 - x - x ^ 2)

Sources

• Knapp, Fibonacci Generating Functions, Journal of Integer Sequences 27 (2024), Article 24.3.1, Lemma 5 (jis-2024-24.3.1-lem-5).

Used by 5

Used byValue of the Gibonacci generating function at one · Value of the Gibonacci generating function at zero · Good rationals for a Gibonacci generating function · One is good for every pair · Zero is good for every pair

TheoremValue of the Gibonacci generating function at zero#✓fully proved

For all integers \(a\) and \(b\), the Gibonacci generating function \(G^{(a,b)}(x) = \frac{(b - a)x + a}{1 - x - x^2}\) takes the value \(G^{(a,b)}(0) = a\) at \(x = 0\).

public theorem gibonacciGeneratingValue_zero (a b : ℤ) :
    gibonacciGeneratingValue a b 0 = (a : ℚ)

Sources

• Knapp, Fibonacci Generating Functions, Journal of Integer Sequences 27 (2024), Article 24.3.1, Lemma 5 (jis-2024-24.3.1-lem-5).

Uses 1 · Used by 1

Statement usesGibonacci generating function

Used byZero is good for every pair

TheoremValue of the Gibonacci generating function at one#✓fully proved

For all integers \(a\) and \(b\), the Gibonacci generating function \(G^{(a,b)}(x) = \frac{(b - a)x + a}{1 - x - x^2}\) takes the value \(G^{(a,b)}(1) = -b\) at \(x = 1\).

public theorem gibonacciGeneratingValue_one (a b : ℤ) :
    gibonacciGeneratingValue a b 1 = -(b : ℚ)

Sources

• Knapp, Fibonacci Generating Functions, Journal of Integer Sequences 27 (2024), Article 24.3.1, Lemma 5 (jis-2024-24.3.1-lem-5).

Uses 1 · Used by 1

Statement usesGibonacci generating function

Used byOne is good for every pair

DefinitionGood rationals for a Gibonacci generating function#✓fully proved

Let \(a\) and \(b\) be integers and let \(G^{(a,b)}(x) = \frac{(b - a)x + a}{1 - x - x^2}\) be the generating function of the Gibonacci sequence with initial terms \(a\) and \(b\). A rational number \(x\) is good for \((a, b)\) when \(1 - x - x^2 \ne 0\) and \(G^{(a,b)}(x)\) is an integer.

public def IsGibonacciGood (a b : ℤ) (x : ℚ) : Prop :=
  1 - x - x ^ 2 ≠ 0 ∧ ∃ z : ℤ, gibonacciGeneratingValue a b x = (z : ℚ)

Sources

• Knapp, Fibonacci Generating Functions, Journal of Integer Sequences 27 (2024), Article 24.3.1 (the paper says x = p / q is good for (a, b) when G^{(a,b)}(x) is an integer; Theorem 1 uses the same integrality without the word good).

Uses 1 · Used by 8

Statement usesGibonacci generating function

Used byConsecutive Fibonacci ratios are good · Congruence criterion for good fractions · One is good for every pair · Good consecutive ratios of a Gibonacci sequence · Consecutive ratios of a shifted Gibonacci sequence are good · Two standard families of good values · Goodness passes to two transformed fractions · Zero is good for every pair

TheoremZero is good for every pair#✓fully proved

For all integers \(a\) and \(b\), the rational number \(0\) is good for \((a, b)\).

public theorem isGibonacciGood_zero (a b : ℤ) : IsGibonacciGood a b 0

Sources

• Knapp, Fibonacci Generating Functions, Journal of Integer Sequences 27 (2024), Article 24.3.1, Lemma 5 (jis-2024-24.3.1-lem-5).

Uses 3

Statement usesGood rationals for a Gibonacci generating function

Proof usesGibonacci generating function · Value of the Gibonacci generating function at zero

TheoremOne is good for every pair#✓fully proved

For all integers \(a\) and \(b\), the rational number \(1\) is good for \((a, b)\).

The value of the Gibonacci generating function there is \(G^{(a,b)}(1) = -b\).

public theorem isGibonacciGood_one (a b : ℤ) : IsGibonacciGood a b 1

Sources

• Knapp, Fibonacci Generating Functions, Journal of Integer Sequences 27 (2024), Article 24.3.1, Lemma 5 (jis-2024-24.3.1-lem-5).

Uses 3

Statement usesGood rationals for a Gibonacci generating function

Proof usesGibonacci generating function · Value of the Gibonacci generating function at one

TheoremGenerating series of a Gibonacci sequence#●ready to prove

Let \(a\) and \(b\) be integers and let \((G_n)_{n \ge 0}\) be the Gibonacci sequence with \(G_0 = a\) and \(G_1 = b\). In the ring \(\mathbb{Q}[[X]]\) of formal power series with rational coefficients,

\[(1 - X - X^2) \sum_{n \ge 0} G_n X^n = a + (b - a) X.\]

This is the product form of the quotient \(\frac{(b - a)x + a}{1 - x - x^2}\) for the generating function of \((G_n)\).

public theorem_wanted gibonacci_powerSeries_mul (a b : ℤ) :
    (1 - PowerSeries.X - PowerSeries.X ^ 2 : PowerSeries ℚ)
        * PowerSeries.mk (fun n => ((gibonacciNumber a b n : ℤ) : ℚ))
      = PowerSeries.C (a : ℚ)
        + PowerSeries.C ((b : ℚ) - (a : ℚ)) * PowerSeries.X

Sources

• Knapp, Fibonacci Generating Functions, Journal of Integer Sequences 27 (2024), Article 24.3.1, Lemma 5 (jis-2024-24.3.1-lem-5).

Uses 1

Statement usesGibonacci numbers

TheoremGoodness passes to two transformed fractions#●ready to prove

Let \(a\), \(b\), \(p\), \(q\) be integers with \(q \ne 0\) and \(\gcd(p, q) = 1\), and suppose that \(p/q\) is good for \((a, b)\). If \(p + q \ne 0\), then \(q/(p + q)\) is good for \((a, b)\); and if \(p \ne 0\), then \((q - p)/p\) is good for \((a, b)\).

public theorem_wanted isGibonacciGood_transform (a b p q : ℤ)
    (hcop : Int.gcd p q = 1) (hq : q ≠ 0)
    (h : IsGibonacciGood a b ((p : ℚ) / (q : ℚ))) :
    (p + q ≠ 0 → IsGibonacciGood a b ((q : ℚ) / ((p : ℚ) + (q : ℚ)))) ∧
    (p ≠ 0 → IsGibonacciGood a b (((q : ℚ) - (p : ℚ)) / (p : ℚ)))

Sources

• Knapp, Fibonacci Generating Functions, Journal of Integer Sequences 27 (2024), Article 24.3.1, Theorem 1 (jis-2024-24.3.1-thm-1).

Uses 1

Statement usesGood rationals for a Gibonacci generating function

TheoremCongruence criterion for good fractions#●ready to prove

Let \(a, b, p, q\) be integers with \((a, b) \ne (0, 0)\), \(q \ne 0\) and \(\gcd(p, q) = 1\), and put \(m = |q^2 - pq - p^2|\). Then \(p / q\) is good for \((a, b)\) if and only if there are integers \(u\) and \(v\) with \((q - p) u \equiv 1\), \(p v \equiv 1\), \(a \equiv -b p u\) and \(a \equiv -b q v \pmod{m}\).

In the source's notation, with modular inverses, the condition reads \(a \equiv -bp(q - p)^{-1} \equiv -bqp^{-1} \pmod{m}\).

public theorem_wanted isGibonacciGood_iff (a b p q : ℤ)
    (hab : (a, b) ≠ (0, 0)) (hcop : Int.gcd p q = 1) (hq : q ≠ 0) :
    IsGibonacciGood a b ((p : ℚ) / (q : ℚ)) ↔
    ∃ u v : ℤ, (q - p) * u ≡ 1 [ZMOD |q ^ 2 - p * q - p ^ 2|] ∧
      p * v ≡ 1 [ZMOD |q ^ 2 - p * q - p ^ 2|] ∧
      a ≡ -b * p * u [ZMOD |q ^ 2 - p * q - p ^ 2|] ∧
      a ≡ -b * q * v [ZMOD |q ^ 2 - p * q - p ^ 2|]

Sources

• Knapp, Fibonacci Generating Functions, Journal of Integer Sequences 27 (2024), Article 24.3.1, Lemma 6 (jis-2024-24.3.1-lem-6).

Uses 1

Statement usesGood rationals for a Gibonacci generating function

TheoremConsecutive Fibonacci ratios are good#●ready to prove

For all integers \(a\) and \(b\) and every natural number \(n\), the ratio \(F_n / F_{n+1}\) of consecutive Fibonacci numbers is good for \((a, b)\).

The source allows every integer \(n \ne -1\), using the Fibonacci numbers at negative indices.

public theorem_wanted isGibonacciGood_fib_div (a b : ℤ) (n : ℕ) :
    IsGibonacciGood a b ((Nat.fib n : ℚ) / (Nat.fib (n + 1) : ℚ))

Sources

• Knapp, Fibonacci Generating Functions, Journal of Integer Sequences 27 (2024), Article 24.3.1, Lemma 7 (jis-2024-24.3.1-lem-7).

Uses 1

Statement usesGood rationals for a Gibonacci generating function

TheoremTwo standard families of good values#●ready to prove

Let \(a\) and \(b\) be integers and let \((G_n)_{n \ge 0}\) be the Gibonacci sequence with \(G_0 = a\) and \(G_1 = b\). For every natural number \(n\), the ratio \(F_n / F_{n+1}\) of consecutive Fibonacci numbers is good for \((a, b)\), and if \(G_n \ne 0\), then \(-G_{n+1} / G_n\) is good for \((a, b)\).

The source indexes both families by all integers (\(n \ne -1\) for the first).

public theorem_wanted isGibonacciGood_standard_values (a b : ℤ) :
    (∀ n : ℕ, IsGibonacciGood a b ((Nat.fib n : ℚ) / (Nat.fib (n + 1) : ℚ))) ∧
    (∀ n : ℕ, gibonacciNumber a b n ≠ 0 →
      IsGibonacciGood a b
        (-(gibonacciNumber a b (n + 1) : ℚ) / (gibonacciNumber a b n : ℚ)))

Sources

• Knapp, Fibonacci Generating Functions, Journal of Integer Sequences 27 (2024), Article 24.3.1, Corollary 2 (jis-2024-24.3.1-cor-2).

Uses 2

Statement usesGood rationals for a Gibonacci generating function · Gibonacci numbers

TheoremConsecutive ratios of a shifted Gibonacci sequence are good#●ready to prove

Let \(a\) and \(b\) be integers and let \((H_n)_{n \ge 0}\) be the Gibonacci sequence with \(H_0 = -b\) and \(H_1 = a\). For every natural number \(n\) with \(H_{n+1} \ne 0\), the ratio \(H_n / H_{n+1}\) is good for \((a, b)\).

The source indexes \(H\) by all integers.

public theorem_wanted isGibonacciGood_shifted_ratio (a b : ℤ) (n : ℕ)
    (h : gibonacciNumber (-b) a (n + 1) ≠ 0) :
    IsGibonacciGood a b
      ((gibonacciNumber (-b) a n : ℚ) / (gibonacciNumber (-b) a (n + 1) : ℚ))

Sources

• Knapp, Fibonacci Generating Functions, Journal of Integer Sequences 27 (2024), Article 24.3.1, Lemma 8 (jis-2024-24.3.1-lem-8).

Uses 2

Statement usesGood rationals for a Gibonacci generating function · Gibonacci numbers

TheoremGood consecutive ratios of a Gibonacci sequence#●ready to prove

Let \(p\) and \(q\) be coprime integers, let \((H_n)_{n \ge 0}\) be the Gibonacci sequence with \(H_0 = p\) and \(H_1 = q\), and put \(m = |q^2 - pq - p^2|\). Call a pair of integers \((a, b)\) admissible when \(H_n / H_{n+1}\) is good for \((a, b)\) for every natural number \(n\) with \(H_{n+1} \ne 0\). Then there are infinitely many admissible pairs, and a pair \((a, b)\) is admissible if and only if there are integers \(u\) and \(v\) with \((q - p) u \equiv 1\), \(p v \equiv 1\), \(a \equiv -b p u\) and \(a \equiv -b q v \pmod{m}\).

In the source's notation, with modular inverses, the condition reads \(a \equiv -bp(q - p)^{-1} \equiv -bqp^{-1} \pmod{m}\). The source indexes \(H\) by all integers.

public theorem_wanted isGibonacciGood_ratios_infinite_iff (p q : ℤ)
    (hcop : Int.gcd p q = 1) :
    (Set.Infinite {ab : ℤ × ℤ | ∀ n : ℕ, gibonacciNumber p q (n + 1) ≠ 0 →
        IsGibonacciGood ab.1 ab.2
          ((gibonacciNumber p q n : ℚ) / (gibonacciNumber p q (n + 1) : ℚ))}) ∧
    ∀ a b : ℤ, (∀ n : ℕ, gibonacciNumber p q (n + 1) ≠ 0 →
        IsGibonacciGood a b
          ((gibonacciNumber p q n : ℚ) / (gibonacciNumber p q (n + 1) : ℚ))) ↔
      ∃ u v : ℤ, (q - p) * u ≡ 1 [ZMOD |q ^ 2 - p * q - p ^ 2|] ∧
        p * v ≡ 1 [ZMOD |q ^ 2 - p * q - p ^ 2|] ∧
        a ≡ -b * p * u [ZMOD |q ^ 2 - p * q - p ^ 2|] ∧
        a ≡ -b * q * v [ZMOD |q ^ 2 - p * q - p ^ 2|]

Sources

• Knapp, Fibonacci Generating Functions, Journal of Integer Sequences 27 (2024), Article 24.3.1, Theorem 3 (jis-2024-24.3.1-thm-3).

Uses 2

Statement usesGood rationals for a Gibonacci generating function · Gibonacci numbers

DefinitionGenerating function of the recurrence \(A_{n+1} = pA_n + A_{n-1}\)#✓fully proved

For integers \(a\), \(b\), \(p\) and a rational number \(x\), \(A(x) = \frac{a(1 - px) + bx}{1 - px - x^2}\), with the convention that a fraction with denominator \(0\) is \(0\). As a rational function, \(A\) is the generating function \(\sum_{n \ge 0} A_n x^n\) of the sequence with \(A_0 = a\), \(A_1 = b\) and \(A_{n+1} = pA_n + A_{n-1}\); for \(p \ne 0\) the denominator \(1 - px - x^2\) has no rational root.

def secondOrderGenValue (a b p : ℤ) (x : ℚ) : ℚ :=
  (a * (1 - p * x) + b * x) / (1 - p * x - x ^ 2)

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Section 2.

Used by 11

Used byA small value of \(M\) in the family of \(r/s\) when \(abp + a^2 - b^2 < 0\) · A small value of \(M\) in the family of \(r/s\) when \(abp + a^2 - b^2 \ge 0\) · Algorithm for integer values of a second-order generating function · Integer values propagate along a family · Integrality criterion at a rational point · Integer values of \(x/(1 - px - x^2)\) come from Lucas ratios · Neighbours of an integer value · Integer values of \((1 - px + x)/(1 - px - x^2)\) · Two families of integer values · Value of the generating function at zero · Rationals where \(x/(1 - px - x^2)\) is an integer

TheoremValue of the generating function at zero#✓fully proved

For all integers \(a, b, p\), the function \(A(x) = \frac{a(1 - px) + bx}{1 - px - x^2}\) on the rationals satisfies \(A(0) = a\).

theorem secondOrderGenValue_zero (a b p : ℤ) : secondOrderGenValue a b p 0 = a

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, proof of Theorem 2.

Uses 1

Statement usesGenerating function of the recurrence \(A_{n+1} = pA_n + A_{n-1}\)

DefinitionForward part of a second-order sequence#✓fully proved

For integers \(p, r, s\), this is the sequence \((A^{(r,s)}_n)_{n \ge 0}\) of integers with \(A^{(r,s)}_0 = r\), \(A^{(r,s)}_1 = s\) and \(A^{(r,s)}_{n+2} = pA^{(r,s)}_{n+1} + A^{(r,s)}_n\) for every natural number \(n\).

def secondOrderFwd (p r s : ℤ) : ℕ → ℤ
  | 0 => r
  | 1 => s
  | n + 2 => p * secondOrderFwd p r s (n + 1) + secondOrderFwd p r s n

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Theorem 1.

Used by 3

Used byEvery rational number lies in its own family · Two-sided second-order sequence · The two-sided sequence satisfies its recurrence at every index

DefinitionBackward part of the two-sided sequence#✓fully proved

For integers \(p\), \(r\) and \(s\), the backward part is the sequence \((B_k)_{k \ge 0}\) with \(B_0 = s\), \(B_1 = r\) and \(B_{k+2} = B_k - pB_{k+1}\). Thus \(B_k\) is the term of index \(1 - k\) of the two-sided sequence with \(A_0 = r\), \(A_1 = s\) and \(A_{n+1} = pA_n + A_{n-1}\), computed backwards by \(A_n = A_{n+2} - pA_{n+1}\).

def secondOrderBwd (p r s : ℤ) : ℕ → ℤ
  | 0 => s
  | 1 => r
  | n + 2 => secondOrderBwd p r s n - p * secondOrderBwd p r s (n + 1)

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Theorem 1.

Used by 4

Used byEvery rational number lies in its own family · Two-sided second-order sequence · The two-sided sequence satisfies its recurrence at every index · First values of the two-sided sequence

DefinitionTwo-sided second-order sequence#✓fully proved

For integers \(p\), \(r\) and \(s\), the two-sided sequence \((A^{(r,s)}_n)_{n \in \mathbb{Z}}\) for \(p\) is the integer sequence indexed by \(\mathbb{Z}\) with \(A^{(r,s)}_0 = r\), \(A^{(r,s)}_1 = s\) and \(A^{(r,s)}_{n+1} = pA^{(r,s)}_n + A^{(r,s)}_{n-1}\) for every integer \(n\).

The paper's forward rule "if \(n > 1\)" is read as \(n \ge 1\), as the definition of \(A_2\) requires.

def secondOrderBiSeq (p r s : ℤ) : ℤ → ℤ
  | (n : ℕ) => secondOrderFwd p r s n
  | Int.negSucc n => secondOrderBwd p r s (n + 2)

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Theorem 1.

Uses 2 · Used by 15

Statement usesBackward part of the two-sided sequence · Forward part of a second-order sequence

Used byTwo-sided binomial sums of products of Lucas sequences · Weighted two-sided binomial sums of products of Lucas sequences · A small value of \(M\) in the family of \(r/s\) when \(abp + a^2 - b^2 < 0\) · A small value of \(M\) in the family of \(r/s\) when \(abp + a^2 - b^2 \ge 0\) · Family generated by a rational number · Every rational number lies in its own family · The two-sided sequence satisfies its recurrence at every index · Second initial value of the two-sided sequence · First values of the two-sided sequence · First initial value of the two-sided sequence · Algorithm for integer values of a second-order generating function · Integer values propagate along a family · Integer values of \((1 - px + x)/(1 - px - x^2)\) · Two families of integer values · Rationals where \(x/(1 - px - x^2)\) is an integer

TheoremFirst values of the two-sided sequence#✓fully proved

For all integers \(p\), \(r\), \(s\), the two-sided sequence \((A^{(r,s)}_n)_{n \in \mathbb{Z}}\) for \(p\) with initial values \(r\) and \(s\) satisfies \(A^{(r,s)}_0 = r\), \(A^{(r,s)}_1 = s\), \(A^{(r,s)}_2 = ps + r\) and \(A^{(r,s)}_{-1} = s - pr\).

theorem secondOrderBiSeq_small (p r s : ℤ) :
    secondOrderBiSeq p r s 0 = r ∧ secondOrderBiSeq p r s 1 = s ∧
      secondOrderBiSeq p r s 2 = p * s + r ∧ secondOrderBiSeq p r s (-1) = s - p * r

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Theorem 1.

Uses 2

Statement usesTwo-sided second-order sequence

Proof usesBackward part of the two-sided sequence

TheoremFirst initial value of the two-sided sequence#✓fully proved

For all integers \(p\), \(r\), \(s\), the two-sided sequence \((A^{(r,s)}_n)_{n \in \mathbb{Z}}\) for \(p\) with initial values \(r\) and \(s\) satisfies \(A^{(r,s)}_0 = r\).

@[simp] theorem secondOrderBiSeq_zero (p r s : ℤ) : secondOrderBiSeq p r s 0 = r

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Theorem 1.

Uses 1

Statement usesTwo-sided second-order sequence

TheoremSecond initial value of the two-sided sequence#✓fully proved

For all integers \(p\), \(r\), \(s\), the two-sided sequence \((A^{(r,s)}_n)_{n \in \mathbb{Z}}\) for \(p\) with initial values \(r\) and \(s\) satisfies \(A^{(r,s)}_1 = s\).

@[simp] theorem secondOrderBiSeq_one (p r s : ℤ) : secondOrderBiSeq p r s 1 = s

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Theorem 1.

Uses 1

Statement usesTwo-sided second-order sequence

TheoremThe two-sided sequence satisfies its recurrence at every index#✓fully proved

Let \(p\), \(r\), \(s\) be integers and \((A^{(r,s)}_n)_{n \in \mathbb{Z}}\) the two-sided sequence for \(p\) with initial values \(A^{(r,s)}_0 = r\) and \(A^{(r,s)}_1 = s\). Then \(A^{(r,s)}_{n+2} = pA^{(r,s)}_{n+1} + A^{(r,s)}_n\) for every integer \(n\).

theorem secondOrderBiSeq_add_two (p r s : ℤ) (n : ℤ) :
    secondOrderBiSeq p r s (n + 2) =
      p * secondOrderBiSeq p r s (n + 1) + secondOrderBiSeq p r s n

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Theorem 1.

Uses 3

Statement usesTwo-sided second-order sequence

Proof usesBackward part of the two-sided sequence · Forward part of a second-order sequence

DefinitionThe quantity \(M(r, s)\) for the recurrence \(A_{n+1} = pA_n + A_{n-1}\)#✓fully proved

For integers \(a\), \(b\), \(p\), \(r\), \(s\), \(M(r, s) = \frac{br^2 + bs^2 - apr^2 + 2ars}{s^2 - prs - r^2}\), a rational number, with the convention that a fraction with denominator \(0\) is \(0\).

When \(s \ne 0\) and \(s^2 - prs - r^2 \ne 0\), write \(k = A(r/s)\), where \(A(x) = \frac{a(1 - px) + bx}{1 - px - x^2}\) is the generating function of the sequence with \(A_0 = a\), \(A_1 = b\) and \(A_{n+1} = pA_n + A_{n-1}\); then \(M(r, s)^2 = (kp + b - ap)^2 - 4k(a - k)\), that is, \(M(r, s) = \pm\sqrt{(kp + b - ap)^2 - 4k(a - k)}\).

def secondOrderMValue (a b p r s : ℤ) : ℚ :=
  (b * r ^ 2 + b * s ^ 2 - a * p * r ^ 2 + 2 * a * r * s) / (s ^ 2 - p * r * s - r ^ 2)

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Section 2 (before Lemma 8).

Used by 4

Used byA small value of \(M\) in the family of \(r/s\) when \(abp + a^2 - b^2 < 0\) · A small value of \(M\) in the family of \(r/s\) when \(abp + a^2 - b^2 \ge 0\) · Relations between values of \(M\) at neighbouring pairs · Value of \(M\) at \((0, 1)\)

TheoremValue of \(M\) at \((0, 1)\)#✓fully proved

For all integers \(a\), \(b\), \(p\), the quantity \(M(r, s) = \frac{br^2 + bs^2 - apr^2 + 2ars}{s^2 - prs - r^2}\) satisfies \(M(0, 1) = b\).

theorem secondOrderMValue_zero_one (a b p : ℤ) : secondOrderMValue a b p 0 1 = b

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Section 2.

Uses 1

Statement usesThe quantity \(M(r, s)\) for the recurrence \(A_{n+1} = pA_n + A_{n-1}\)

DefinitionFamily generated by a rational number#✓fully proved

Let \(p\) be an integer and \(x_0\) a rational number, written \(x_0 = r/s\) in lowest terms with \(s > 0\), and let \((A^{(r,s)}_n)_{n \in \mathbb{Z}}\) be the two-sided sequence with \(A^{(r,s)}_0 = r\), \(A^{(r,s)}_1 = s\) and \(A^{(r,s)}_{n+1} = pA^{(r,s)}_n + A^{(r,s)}_{n-1}\). A rational number \(x\) belongs to the family generated by \(x_0\) when there is an integer \(n\) with \(A^{(r,s)}_{n+1} \ne 0\) and \(x = A^{(r,s)}_n / A^{(r,s)}_{n+1}\).

def IsInSecondOrderFamily (p : ℤ) (x₀ x : ℚ) : Prop :=
  ∃ n : ℤ, secondOrderBiSeq p x₀.num x₀.den (n + 1) ≠ 0 ∧
    x = (secondOrderBiSeq p x₀.num x₀.den n : ℚ) / secondOrderBiSeq p x₀.num x₀.den (n + 1)

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Theorem 1 and Remark 7(ii).

Uses 1 · Used by 2

Statement usesTwo-sided second-order sequence

Used byEvery rational number lies in its own family · Algorithm for integer values of a second-order generating function

TheoremEvery rational number lies in its own family#✓fully proved

For every integer \(p\) and every rational number \(x_0\), \(x_0\) belongs to the family generated by \(x_0\) for \(p\).

theorem isInSecondOrderFamily_self (p : ℤ) (x₀ : ℚ) : IsInSecondOrderFamily p x₀ x₀

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Theorem 1.

Uses 4

Statement usesFamily generated by a rational number

Proof usesTwo-sided second-order sequence · Backward part of the two-sided sequence · Forward part of a second-order sequence

TheoremInteger values propagate along a family#●ready to prove

Let \(a, b, p\) be integers with \(p \ne 0\), let \(A(x) = \frac{a(1 - px) + bx}{1 - px - x^2}\) for rational \(x\), and for integers \(r, s\) let \(A^{(r,s)}\) be the two-sided integer sequence with \(A^{(r,s)}_0 = r\), \(A^{(r,s)}_1 = s\) and \(A^{(r,s)}_{n+2} = pA^{(r,s)}_{n+1} + A^{(r,s)}_n\) for all integers \(n\). If \(r\) and \(s\) are coprime integers with \(s \ne 0\) and \(A(r/s)\) is an integer, then \(A(A^{(r,s)}_n / A^{(r,s)}_{n+1})\) is an integer for every integer \(n\) with \(A^{(r,s)}_{n+1} \ne 0\).

public theorem_wanted secondOrderGenValue_family_integer (a b p : ℤ) (hp : p ≠ 0) (r s : ℤ)
    (hs : s ≠ 0)
    (hrs : Int.gcd r s = 1) (hint : ∃ z : ℤ, secondOrderGenValue a b p ((r : ℚ) / s) = z)
    (n : ℤ) (hn : secondOrderBiSeq p r s (n + 1) ≠ 0) :
    ∃ z : ℤ, secondOrderGenValue a b p
      ((secondOrderBiSeq p r s n : ℚ) / secondOrderBiSeq p r s (n + 1)) = z

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Theorem 1 (jis-2025-25.8.3-thm-1).

Uses 2

Statement usesTwo-sided second-order sequence · Generating function of the recurrence \(A_{n+1} = pA_n + A_{n-1}\)

TheoremTwo families of integer values#●ready to prove

Let \(a, b, p\) be integers with \(p \ne 0\), let \(A(x) = \frac{a(1 - px) + bx}{1 - px - x^2}\) for rational \(x\), and for integers \(r, s\) let \(A^{(r,s)}\) be the two-sided integer sequence with \(A^{(r,s)}_0 = r\), \(A^{(r,s)}_1 = s\) and \(A^{(r,s)}_{n+2} = pA^{(r,s)}_{n+1} + A^{(r,s)}_n\) for all integers \(n\). Then \(A(A^{(0,1)}_n / A^{(0,1)}_{n+1})\) is an integer for every integer \(n \ne -1\), and \(A(A^{(-b,a)}_n / A^{(-b,a)}_{n+1})\) is an integer for every integer \(n\) with \(A^{(-b,a)}_{n+1} \ne 0\).

public theorem_wanted secondOrderGenValue_trivial_families_integer (a b p : ℤ) (hp : p ≠ 0) :
    (∀ n : ℤ, n ≠ -1 → ∃ z : ℤ, secondOrderGenValue a b p
      ((secondOrderBiSeq p 0 1 n : ℚ) / secondOrderBiSeq p 0 1 (n + 1)) = z) ∧
    ∀ n : ℤ, secondOrderBiSeq p (-b) a (n + 1) ≠ 0 → ∃ z : ℤ, secondOrderGenValue a b p
      ((secondOrderBiSeq p (-b) a n : ℚ) / secondOrderBiSeq p (-b) a (n + 1)) = z

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Theorem 2 (jis-2025-25.8.3-thm-2).

Uses 2

Statement usesTwo-sided second-order sequence · Generating function of the recurrence \(A_{n+1} = pA_n + A_{n-1}\)

TheoremIntegrality criterion at a rational point#●ready to prove

Let \(a, b, p\) be integers with \(p \ne 0\) and let \(A(x) = \frac{a(1 - px) + bx}{1 - px - x^2}\) for rational \(x\). Let \(r, s\) be coprime integers with \(s \ne 0\) and put \(D = s^2 - prs - r^2\). Then \(A(r/s)\) is an integer if and only if \(b \equiv -art \pmod{D}\) for every integer \(t\) with \(st \equiv 1 \pmod{D}\).

Since \(s\) is invertible modulo \(D\), this is the congruence \(b \equiv -ars^{-1} \pmod{|D|}\).

public theorem_wanted secondOrderGenValue_integer_iff (a b p : ℤ) (hp : p ≠ 0) (r s : ℤ)
    (hs : s ≠ 0)
    (hrs : Int.gcd r s = 1) :
    (∃ z : ℤ, secondOrderGenValue a b p ((r : ℚ) / s) = z) ↔
      ∀ t : ℤ, s * t ≡ 1 [ZMOD (s ^ 2 - p * r * s - r ^ 2)] →
        b ≡ -a * r * t [ZMOD (s ^ 2 - p * r * s - r ^ 2)]

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Lemma 4 (jis-2025-25.8.3-lem-4).

Uses 1

Statement usesGenerating function of the recurrence \(A_{n+1} = pA_n + A_{n-1}\)

TheoremNeighbours of an integer value#●ready to prove

Let \(a, b, p\) be integers with \(p \ne 0\) and let \(A(x) = \frac{a(1 - px) + bx}{1 - px - x^2}\) for rational \(x\). If \(r, s\) are coprime integers with \(r \ne 0\), \(s \ne 0\) and \(r + ps \ne 0\), and \(A(r/s)\) is an integer, then \(A(s/(r + ps))\) and \(A((s - pr)/r)\) are integers.

public theorem_wanted secondOrderGenValue_neighbors_integer (a b p : ℤ) (hp : p ≠ 0) (r s : ℤ)
    (hr : r ≠ 0)
    (hs : s ≠ 0) (hrps : r + p * s ≠ 0) (hrs : Int.gcd r s = 1)
    (hint : ∃ z : ℤ, secondOrderGenValue a b p ((r : ℚ) / s) = z) :
    (∃ z : ℤ, secondOrderGenValue a b p ((s : ℚ) / (r + p * s)) = z) ∧
      ∃ z : ℤ, secondOrderGenValue a b p (((s : ℚ) - p * r) / r) = z

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Lemma 6 (jis-2025-25.8.3-lem-6).

Uses 1

Statement usesGenerating function of the recurrence \(A_{n+1} = pA_n + A_{n-1}\)

TheoremRelations between values of \(M\) at neighbouring pairs#●ready to prove

Let \(a\), \(b\), \(p\) be integers with \(p \ne 0\), and for integers \(r\), \(s\) let \(M(r, s) = \frac{br^2 + bs^2 - apr^2 + 2ars}{s^2 - prs - r^2}\). Then for all integers \(r\), \(s\) that are not both zero, \(M(s - pr, r) + (p^2 + 2)M(r, s) + M(s, r + ps) = 0\) and \(M(r, s)^2 + (p^2 + 2)M(r, s)M(s, r + ps) + M(s, r + ps)^2 = abp^3 + (a^2 - b^2)p^2\).

The source assumes \(r \ne 0\), \(s \ne 0\) and \(r + ps \ne 0\); here only \((r, s) \ne (0, 0)\) is assumed. Since \(p \ne 0\), the three denominators equal \(\pm(s^2 - prs - r^2)\), which is nonzero.

public theorem_wanted secondOrderMValue_relations (a b p : ℤ) (hp : p ≠ 0) (r s : ℤ) (hrs :
    (r, s) ≠ (0, 0)) :
    secondOrderMValue a b p (s - p * r) r + (p ^ 2 + 2) * secondOrderMValue a b p r s +
        secondOrderMValue a b p s (r + p * s) = 0 ∧
      secondOrderMValue a b p r s ^ 2 +
          (p ^ 2 + 2) * secondOrderMValue a b p r s * secondOrderMValue a b p s (r + p * s) +
          secondOrderMValue a b p s (r + p * s) ^ 2 =
        a * b * p ^ 3 + (a ^ 2 - b ^ 2) * p ^ 2

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Lemma 8 (jis-2025-25.8.3-lem-8).

Uses 1

Statement usesThe quantity \(M(r, s)\) for the recurrence \(A_{n+1} = pA_n + A_{n-1}\)

TheoremA small value of \(M\) in the family of \(r/s\) when \(abp + a^2 - b^2 < 0\)#●ready to prove

Let \(a, b, p\) be integers with \(p \ne 0\) and \(abp + a^2 - b^2 < 0\). Let \(A(x) = \frac{a(1 - px) + bx}{1 - px - x^2}\) for rational \(x\), and for integers \(u, v\) let \(M(u, v) = \frac{bu^2 + bv^2 - apu^2 + 2auv}{v^2 - puv - u^2}\), where in both a fraction with denominator \(0\) is read as \(0\). Let \(r, s\) be coprime integers with \(s \ne 0\) such that \(A(r/s)\) is an integer, and let \((A^{(r,s)}_n)_{n \in \mathbb{Z}}\) be the two-sided sequence with \(A^{(r,s)}_0 = r\), \(A^{(r,s)}_1 = s\) and \(A^{(r,s)}_{n+1} = pA^{(r,s)}_n + A^{(r,s)}_{n-1}\) for every integer \(n\). If \(A^{(r,s)}_n \ne 0\) for every integer \(n\), then there is an integer \(n\) with \(|M(A^{(r,s)}_n, A^{(r,s)}_{n+1})| \le \sqrt{b^2 - a^2 - abp}\).

The hypothesis that no term vanishes is the paper's assumption before Lemma 8 ("we can assume that the conditions \(r \ne 0, s \ne 0, r + ps \ne 0\) automatically hold"). Without it the paper's claim fails: for \((a, b, p) = (-1, 8, -1)\) and \(x = 0\), the members \(A_n/A_{n+1}\) of the family \(A^{(0,1)}\) with \(A_{n+1} \ne 0\) have \(\min |M| = 8 > \sqrt{55}\).

public theorem_wanted exists_small_secondOrderMValue_of_neg (a b p : ℤ) (hp : p ≠ 0)
    (hneg : a * b * p + a ^ 2 - b ^ 2 < 0) (r s : ℤ) (hs : s ≠ 0) (hrs : Int.gcd r s = 1)
    (hint : ∃ z : ℤ, secondOrderGenValue a b p ((r : ℚ) / s) = z)
    (hnz : ∀ n : ℤ, secondOrderBiSeq p r s n ≠ 0) :
    ∃ n : ℤ, |(secondOrderMValue a b p (secondOrderBiSeq p r s n)
        (secondOrderBiSeq p r s (n + 1)) : ℝ)| ≤ √((-a * b * p - a ^ 2 + b ^ 2 : ℤ) : ℝ)

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Lemma 9 (jis-2025-25.8.3-lem-9).

Uses 3

Statement usesTwo-sided second-order sequence · Generating function of the recurrence \(A_{n+1} = pA_n + A_{n-1}\) · The quantity \(M(r, s)\) for the recurrence \(A_{n+1} = pA_n + A_{n-1}\)

TheoremA small value of \(M\) in the family of \(r/s\) when \(abp + a^2 - b^2 \ge 0\)#●ready to prove

Let \(a, b, p\) be integers with \(p \ne 0\) and \(abp + a^2 - b^2 \ge 0\). Let \(A(x) = \frac{a(1 - px) + bx}{1 - px - x^2}\) for rational \(x\), and for integers \(u, v\) let \(M(u, v) = \frac{bu^2 + bv^2 - apu^2 + 2auv}{v^2 - puv - u^2}\), where in both a fraction with denominator \(0\) is read as \(0\). Let \(r, s\) be coprime integers with \(s \ne 0\) such that \(A(r/s)\) is an integer, and let \((A^{(r,s)}_n)_{n \in \mathbb{Z}}\) be the two-sided sequence with \(A^{(r,s)}_0 = r\), \(A^{(r,s)}_1 = s\) and \(A^{(r,s)}_{n+1} = pA^{(r,s)}_n + A^{(r,s)}_{n-1}\) for every integer \(n\). If \(A^{(r,s)}_n \ne 0\) for every integer \(n\), then there is an integer \(n\) with \(|M(A^{(r,s)}_n, A^{(r,s)}_{n+1})| \le \sqrt{(abp^3 + (a^2 - b^2)p^2)/(p^2 + 4)}\).

The hypothesis that no term vanishes is the paper's assumption before Lemma 8. Without it the paper's claim fails: for \((a, b, p) = (-3, -8, 5)\) and \(x = 0\), the members \(A_n/A_{n+1}\) of the family \(A^{(0,1)}\) with \(A_{n+1} \ne 0\) have \(\min |M| = 8\), while \((abp^3 + (a^2 - b^2)p^2)/(p^2 + 4) = 1625/29 < 64\).

public theorem_wanted exists_small_secondOrderMValue_of_nonneg (a b p : ℤ) (hp : p ≠ 0)
    (hnonneg : 0 ≤ a * b * p + a ^ 2 - b ^ 2) (r s : ℤ) (hs : s ≠ 0) (hrs : Int.gcd r s = 1)
    (hint : ∃ z : ℤ, secondOrderGenValue a b p ((r : ℚ) / s) = z)
    (hnz : ∀ n : ℤ, secondOrderBiSeq p r s n ≠ 0) :
    ∃ n : ℤ, |(secondOrderMValue a b p (secondOrderBiSeq p r s n)
        (secondOrderBiSeq p r s (n + 1)) : ℝ)| ≤
      √(((a * b * p ^ 3 + (a ^ 2 - b ^ 2) * p ^ 2 : ℤ) : ℝ) / (p ^ 2 + 4))

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Lemma 10 (jis-2025-25.8.3-lem-10).

Uses 3

Statement usesTwo-sided second-order sequence · Generating function of the recurrence \(A_{n+1} = pA_n + A_{n-1}\) · The quantity \(M(r, s)\) for the recurrence \(A_{n+1} = pA_n + A_{n-1}\)

TheoremAlgorithm for integer values of a second-order generating function#●ready to prove

Let \(a, b, p\) be integers with \(p \ne 0\) and \((a, b) \ne (0, 0)\), let \(A(x) = \frac{a(1 - px) + bx}{1 - px - x^2}\) for rational \(x\), and for integers \(r, s\) let \(A^{(r,s)}\) be the two-sided integer sequence with \(A^{(r,s)}_0 = r\), \(A^{(r,s)}_1 = s\) and \(A^{(r,s)}_{n+2} = pA^{(r,s)}_{n+1} + A^{(r,s)}_n\) for all integers \(n\). Put \(E = abp^3 + (a^2 - b^2)p^2\), and let \(B = E/(p^2 + 4)\) if \(E \ge 0\) and \(B = -abp + b^2 - a^2\) if \(E < 0\). (Soundness) If \(M\) and \(k\) are integers with \(k \ne 0\) and \(M^2 = (kp - ap + b)^2 - 4k(a - k)\), then \(A(x)\) is an integer for both \(x = (ap - kp - b + M)/(2k)\) and \(x = (ap - kp - b - M)/(2k)\). (Completeness) If \(x\) is a rational number for which \(A(x)\) is an integer, then at least one of the following holds: there is an integer \(n\) with \(A^{(0,1)}_{n+1} \ne 0\) and \(x = A^{(0,1)}_n / A^{(0,1)}_{n+1}\); there is an integer \(n\) with \(A^{(-b,a)}_{n+1} \ne 0\) and \(x = A^{(-b,a)}_n / A^{(-b,a)}_{n+1}\); or there are integers \(M, N, k\) with \(M^2 \le B\), \(M^2 + (p^2 + 2)MN + N^2 = E\), \(k \ne 0\) and \(M^2 = (kp - ap + b)^2 - 4k(a - k)\), and a rational number \(x' \in \{(ap - kp - b + M)/(2k), (ap - kp - b - M)/(2k)\}\) such that \(x\) lies in the family of \(x'\): writing \(x' = u/v\) in lowest terms with \(v > 0\), there is an integer \(n\) with \(A^{(u,v)}_{n+1} \ne 0\) and \(x = A^{(u,v)}_n / A^{(u,v)}_{n+1}\).

The bound \(M^2 \le B\) is the condition \(|M| \le \sqrt{B}\) of the source.

MetaMathlibExt.secondOrderGenValue_algorithm · 18 lines

public theorem_wanted secondOrderGenValue_algorithm (a b p : ℤ) (hp : p ≠ 0) (hab : (a, b) ≠
    (0, 0)) :
    (∀ M k : ℤ, k ≠ 0 → M ^ 2 = (k * p - a * p + b) ^ 2 - 4 * k * (a - k) →
      ∀ x : ℚ, (x = (a * p - k * p - b + M) / (2 * k) ∨ x = (a * p - k * p - b - M) / (2 * k)) →
        ∃ z : ℤ, secondOrderGenValue a b p x = z) ∧
    ∀ x : ℚ, (∃ z : ℤ, secondOrderGenValue a b p x = z) →
      (∃ n : ℤ, secondOrderBiSeq p 0 1 (n + 1) ≠ 0 ∧
        x = (secondOrderBiSeq p 0 1 n : ℚ) / secondOrderBiSeq p 0 1 (n + 1)) ∨
      (∃ n : ℤ, secondOrderBiSeq p (-b) a (n + 1) ≠ 0 ∧
        x = (secondOrderBiSeq p (-b) a n : ℚ) / secondOrderBiSeq p (-b) a (n + 1)) ∨
      ∃ M N k : ℤ,
        ((M : ℝ) ^ 2 ≤ if 0 ≤ a * b * p ^ 3 + (a ^ 2 - b ^ 2) * p ^ 2 then
          ((a * b * p ^ 3 + (a ^ 2 - b ^ 2) * p ^ 2 : ℤ) : ℝ) / (p ^ 2 + 4)
          else ((-a * b * p + b ^ 2 - a ^ 2 : ℤ) : ℝ)) ∧
        M ^ 2 + (p ^ 2 + 2) * M * N + N ^ 2 = a * b * p ^ 3 + (a ^ 2 - b ^ 2) * p ^ 2 ∧
        k ≠ 0 ∧ M ^ 2 = (k * p - a * p + b) ^ 2 - 4 * k * (a - k) ∧
        ∃ x' : ℚ, (x' = (a * p - k * p - b + M) / (2 * k) ∨
          x' = (a * p - k * p - b - M) / (2 * k)) ∧ IsInSecondOrderFamily p x' x

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Theorem 3 (jis-2025-25.8.3-thm-3).

Uses 3

Statement usesFamily generated by a rational number · Two-sided second-order sequence · Generating function of the recurrence \(A_{n+1} = pA_n + A_{n-1}\)

TheoremRationals where \(x/(1 - px - x^2)\) is an integer#●ready to prove

Let \(p \ne 0\) be an integer, let \(G(x) = \frac{x}{1 - px - x^2}\) for rational \(x\), and let \(A^{(0,1)}\) be the two-sided integer sequence with \(A^{(0,1)}_0 = 0\), \(A^{(0,1)}_1 = 1\) and \(A^{(0,1)}_{n+2} = pA^{(0,1)}_{n+1} + A^{(0,1)}_n\) for all integers \(n\). Then the set of rational numbers \(x\) for which \(G(x)\) is an integer is \(\{A^{(0,1)}_n / A^{(0,1)}_{n+1} : n \in \mathbb{Z},\ n \ne -1\}\).

public theorem_wanted secondOrderGenValue_zero_one_integer_set (p : ℤ) (hp : p ≠ 0) :
    {x : ℚ | ∃ z : ℤ, secondOrderGenValue 0 1 p x = z} =
      {x | ∃ n : ℤ, n ≠ -1 ∧
        x = (secondOrderBiSeq p 0 1 n : ℚ) / secondOrderBiSeq p 0 1 (n + 1)}

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Corollary 13 (jis-2025-25.8.3-cor-13).

Uses 2

Statement usesTwo-sided second-order sequence · Generating function of the recurrence \(A_{n+1} = pA_n + A_{n-1}\)

TheoremInteger values of \(x/(1 - px - x^2)\) come from Lucas ratios#●ready to prove

Let \(p \ne 0\) be an integer, let \((U_n)_{n \ge 0}\) be the Lucas sequence \(U(p, -1)\), so \(U_0 = 0\), \(U_1 = 1\) and \(U_{n+2} = pU_{n+1} + U_n\), and let \(G(x) = \frac{x}{1 - px - x^2}\) for rational \(x\). Then \(G(U_n/U_{n+1})\) is an integer for every natural number \(n\); and if \(G(x) = k\) for a rational number \(x\) and an integer \(k\), then \(G(U_n/U_{n+1}) = k\) for some natural number \(n\).

public theorem_wanted secondOrderGenValue_lucasU (p : ℤ) (hp : p ≠ 0) :
    (∀ n : ℕ, ∃ z : ℤ, secondOrderGenValue 0 1 p
      ((lucasU ⟨p, -1, by norm_num⟩ n : ℚ) / lucasU ⟨p, -1, by norm_num⟩ (n + 1)) = z) ∧
    ∀ (x : ℚ) (k : ℤ), secondOrderGenValue 0 1 p x = k → ∃ n : ℕ, secondOrderGenValue 0 1 p
      ((lucasU ⟨p, -1, by norm_num⟩ n : ℚ) / lucasU ⟨p, -1, by norm_num⟩ (n + 1)) = k

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Corollary 14 (jis-2025-25.8.3-cor-14).

Uses 3

Statement usesParameters of a Lucas sequence · Lucas sequence \(U(P, Q)\) · Generating function of the recurrence \(A_{n+1} = pA_n + A_{n-1}\)

TheoremInteger values of \((1 - px + x)/(1 - px - x^2)\)#●ready to prove

Let \(p \ne 0\) be an integer, let \(A(x) = \frac{1 - px + x}{1 - px - x^2}\) for rational \(x\), and for integers \(r, s\) let \(A^{(r,s)}\) be the two-sided integer sequence with \(A^{(r,s)}_0 = r\), \(A^{(r,s)}_1 = s\) and \(A^{(r,s)}_{n+2} = pA^{(r,s)}_{n+1} + A^{(r,s)}_n\) for all integers \(n\). If \(x\) is a rational number for which \(A(x)\) is an integer, then there is an integer \(n\) with \(A^{(0,1)}_{n+1} \ne 0\) and \(x = A^{(0,1)}_n / A^{(0,1)}_{n+1}\), or there is an integer \(n\) with \(A^{(-1,1)}_{n+1} \ne 0\) and \(x = A^{(-1,1)}_n / A^{(-1,1)}_{n+1}\).

public theorem_wanted secondOrderGenValue_one_one_families (p : ℤ) (hp : p ≠ 0) (x : ℚ)
    (hx : ∃ z : ℤ, secondOrderGenValue 1 1 p x = z) :
    (∃ n : ℤ, secondOrderBiSeq p 0 1 (n + 1) ≠ 0 ∧
      x = (secondOrderBiSeq p 0 1 n : ℚ) / secondOrderBiSeq p 0 1 (n + 1)) ∨
    ∃ n : ℤ, secondOrderBiSeq p (-1) 1 (n + 1) ≠ 0 ∧
      x = (secondOrderBiSeq p (-1) 1 n : ℚ) / secondOrderBiSeq p (-1) 1 (n + 1)

Sources

• Luu Ba Thang and Nguyen Duy Nguyen, Integer Values of Generating Functions for a Type of Second-Order Linear Recurrence Sequence, Journal of Integer Sequences 28 (2025), Article 25.8.3, Corollary 15 (jis-2025-25.8.3-cor-15).

Uses 2

Statement usesTwo-sided second-order sequence · Generating function of the recurrence \(A_{n+1} = pA_n + A_{n-1}\)

19 fully proved18 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.