Cubic analogues of Lucas sequences

DefinitionRoot condition for the Roettger–Williams cubic#✓fully proved

For integers \(S_1, S_2, R\) and a complex number \(\gamma\), put \(\rho = R(\gamma + \gamma^{-1})\) (with the convention \(0^{-1} = 0\)) and \(S_3 = RS_1^2 - 2RS_2 - 4R^3\). The root condition holds when \(\rho\) is a root of the cubic \(x^3 - S_1x^2 + S_2x - S_3\), that is, when \(\rho^3 - S_1\rho^2 + S_2\rho - S_3 = 0\).

def cubicRecurrenceRootCondition (S₁ S₂ R : ℤ) (γ : ℂ) : Prop :=
  let ρ := (R : ℂ) * (γ + γ⁻¹)
  let S₃ : ℤ := R * S₁ ^ 2 - 2 * R * S₂ - 4 * R ^ 3
  ρ ^ 3 - (S₁ : ℂ) * ρ ^ 2 + (S₂ : ℂ) * ρ - (S₃ : ℂ) = 0
Used by 2
Used byDivisibility of the cubic-recurrence discriminants · Cubic recurrence pair

DefinitionCubic recurrence pair#✓fully proved

Integer sequences \(U\) and \(W\) form a cubic recurrence pair for integers \(S_1, S_2, R\) when there are pairwise distinct complex numbers \(\gamma_1, \gamma_2, \gamma_3\), each different from \(1\), with \(\gamma_1\gamma_2\gamma_3 = 1\), such that each \(\gamma_i\) satisfies the cubic recurrence root condition for \((S_1, S_2, R)\), \(U_0 = 0\), \(U_n(1 - \gamma_1)(1 - \gamma_2)(1 - \gamma_3) = R^{n-1}(1 - \gamma_1^n)(1 - \gamma_2^n) (1 - \gamma_3^n)\) for every \(n \ge 1\), and \(W_n = R^n\bigl((1 + \gamma_1^n)(1 + \gamma_2^n)(1 + \gamma_3^n) - 2\bigr)\) for every \(n \ge 0\).

These equations determine every value of \(U\) and \(W\); the equation for \(U_n\) is the source's formula with its denominator \((1 - \gamma_1)(1 - \gamma_2)(1 - \gamma_3)\) cleared.

MetaMathlibExt.IsCubicRecurrencePair · 18 lines 
def IsCubicRecurrencePair
    (S₁ S₂ R : ℤ) (U W : ℕ → ℤ) : Prop :=
  ∃ γ₁ γ₂ γ₃ : ℂ,
    γ₁ ≠ 1 ∧ γ₂ ≠ 1 ∧ γ₃ ≠ 1 ∧
    γ₁ ≠ γ₂ ∧ γ₂ ≠ γ₃ ∧ γ₃ ≠ γ₁ ∧
    γ₁ * γ₂ * γ₃ = 1 ∧
    cubicRecurrenceRootCondition S₁ S₂ R γ₁ ∧
    cubicRecurrenceRootCondition S₁ S₂ R γ₂ ∧
    cubicRecurrenceRootCondition S₁ S₂ R γ₃ ∧
    U 0 = 0 ∧
    (∀ n : ℕ, 1 ≤ n →
      (U n : ℂ) * ((1 - γ₁) * (1 - γ₂) * (1 - γ₃)) =
        (R : ℂ) ^ (n - 1) *
          ((1 - γ₁ ^ n) * (1 - γ₂ ^ n) * (1 - γ₃ ^ n))) ∧
    ∀ n : ℕ,
      (W n : ℂ) =
        (R : ℂ) ^ n *
          ((1 + γ₁ ^ n) * (1 + γ₂ ^ n) * (1 + γ₃ ^ n) - 2)
Uses 1 · Used by 1
Statement usesRoot condition for the Roettger–Williams cubic
Used byDivisibility of the cubic-recurrence discriminants

DefinitionCubic-recurrence discriminant sequence#✓fully proved

For an integer \(R\) and integer sequences \(U\) and \(W\), the discriminant sequence is \(D_n = \gcd(W_n - 6R^n, U_n)\) for \(n \ge 0\): the greatest common divisor of the natural numbers \(|W_n - 6R^n|\) and \(|U_n|\).

def cubicRecurrenceDiscriminant (R : ℤ) (U W : ℕ → ℤ) (n : ℕ) : ℕ :=
  Nat.gcd (W n - 6 * R ^ n).natAbs (U n).natAbs
Used by 1
Used byDivisibility of the cubic-recurrence discriminants

TheoremDivisibility of the cubic-recurrence discriminants#✓fully proved

Let \(S_1, S_2, R\) be integers, let \(U\) and \(W\) be integer sequences forming a cubic recurrence pair for \((S_1, S_2, R)\), and let \(D_n = \gcd(W_n - 6R^n, U_n)\) be their discriminant sequence. Then for all integers \(n \ge 1\) and \(m \ge 1\), \(D_n\) divides \(D_{nm}\).

theorem cubicRecurrenceDiscriminant_dvd_mul
    (S₁ S₂ R : ℤ) (U W : ℕ → ℤ)
    (hseq : IsCubicRecurrencePair S₁ S₂ R U W)
    (n m : ℕ) (hn : 1 ≤ n) (hm : 1 ≤ m) :
    cubicRecurrenceDiscriminant R U W n ∣
      cubicRecurrenceDiscriminant R U W (n * m)
Sources
Uses 3
Statement usesCubic recurrence pair · Cubic-recurrence discriminant sequence
Proof usesRoot condition for the Roettger–Williams cubic
4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.