Nonlinear floor recurrences satisfying linear recurrences

DefinitionThe sequence OEIS A022030#✓fully proved

The sequence of natural numbers with \(a(0) = 4\), \(a(1) = 16\) and, for every natural number \(n\), \(a(n + 2) = \lfloor (a(n + 1)^2 + a(n) - 1) / a(n) \rfloor - 1\) if \(n\) is even and \(a(n + 2) = \lfloor a(n + 1)^2 / a(n) \rfloor + 1\) if \(n\) is odd.

def a (n : ℕ) : ℕ :=
  match n with
  | 0 => 4
  | 1 => 16
  | n + 2 =>
    if Even n then
      (a (n + 1) ^ 2 + a n - 1) / a n - 1
    else
      (a (n + 1) ^ 2) / a n + 1

Used by 1

Used byBarker's linear recurrence for A022030

DefinitionBarker's linear recurrence for A022030#✓fully proved

The statement that for every natural number \(n \ge 4\), the sequence \(a\) of OEIS A022030 satisfies \(a(n) = 4a(n - 1) - a(n - 3) + a(n - 4)\), with the subtraction taken in the natural numbers (truncated at \(0\)).

def conjecture : Prop :=
  ∀ (n : ℕ) (_hn : 4 ≤ n),
    a n = 4 * a (n - 1) - a (n - 3) + a (n - 4)

def a (n : ℕ) : ℕ :=
  match n with
  | 0 => 4
  | 1 => 16
  | n + 2 =>
    if Even n then
      (a (n + 1) ^ 2 + a n - 1) / a n - 1
    else
      (a (n + 1) ^ 2) / a n + 1

WantedExt/NumberTheory/OeisA022030Wanted.lean:30

Uses 1 · Used by 1

Statement usesThe sequence OEIS A022030

Used byBarker's linear recurrence for A022030 holds

TheoremBarker's linear recurrence for A022030 holds#●ready to prove

For every natural number \(n \ge 4\), the sequence \(a\) of OEIS A022030 satisfies \(a(n) = 4a(n - 1) - a(n - 3) + a(n - 4)\), with the subtraction taken in the natural numbers (truncated at \(0\)).

public theorem_wanted conjecture_holds : conjecture

Sources

Kenta Kitamura, Lean formal proof of Barker's linear recurrence, https://github.com/KitaKen1/oeis-a022030-lean/blob/f74afc2/lean/OeisA022030FC.lean#L270-L275.

Uses 1

Statement usesBarker's linear recurrence for A022030

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.