Shakov's 2-regular sequence

DefinitionShakov's \(2\)-regular sequence#✓fully proved

The integer sequence \(s\) with \(s(0) = s(1) = 0\), \(s(2) = s(3) = 1\) and, for every \(k \ge 1\), \(s(4k) = 2s(2k) - s(k)\), \(s(4k+1) = 2s(2k) + s(2k+1)\), \(s(4k+2) = 2s(2k+1) + s(2k)\) and \(s(4k+3) = 2s(2k+1) - s(k)\).

The value \(s(0)\) plays no role in the recursion; the source's sequence starts at \(n = 1\).

MathlibExt.NumberTheory.ShakovTwoRegularWanted.shakovSeq · 18 lines

def shakovSeq : ℕ → ℤ
  | 0 => 0
  | 1 => 0
  | 2 => 1
  | 3 => 1
  | n + 4 =>
      if (n + 4) % 4 = 0 then
        2 * shakovSeq (2 * ((n + 4) / 4)) - shakovSeq ((n + 4) / 4)
      else if (n + 4) % 4 = 1 then
        2 * shakovSeq (2 * ((n + 4) / 4)) +
          shakovSeq (2 * ((n + 4) / 4) + 1)
      else if (n + 4) % 4 = 2 then
        2 * shakovSeq (2 * ((n + 4) / 4) + 1) +
          shakovSeq (2 * ((n + 4) / 4))
      else
        2 * shakovSeq (2 * ((n + 4) / 4) + 1) - shakovSeq ((n + 4) / 4)
  termination_by n => n
  decreasing_by all_goals omega

Used by 4

Used byBlock averages of Shakov's sequence · Shakov's sequence counts the divisors of \(m^2 + 1\) · Primality of \(n^2 + 1\) from the fibers of Shakov's sequence · Shakov's sequence takes Fibonacci values along the auxiliary sequence

DefinitionShakov's auxiliary sequence#✓fully proved

The integer sequence \(a\) with \(a(0) = 0\), \(a(1) = 1\) and, for every \(n \ge 2\), \(a(n) = 2a(n-1)\) if \(n \equiv 0 \pmod 4\), \(a(n) = a(n-1) + 1\) if \(n \equiv 1 \pmod 4\), \(a(n) = 2a(n-1) + 1\) if \(n \equiv 2 \pmod 4\), and \(a(n) = a(n-1) - 1\) if \(n \equiv 3 \pmod 4\).

The value \(a(0)\) plays no role in the recursion; the source's sequence starts at \(n = 1\).

def shakovA : ℕ → ℤ
  | 0 => 0
  | 1 => 1
  | n + 2 =>
      if (n + 2) % 4 = 0 then 2 * shakovA (n + 1)
      else if (n + 2) % 4 = 1 then shakovA (n + 1) + 1
      else if (n + 2) % 4 = 2 then 2 * shakovA (n + 1) + 1
      else shakovA (n + 1) - 1

Used by 1

Used byShakov's sequence takes Fibonacci values along the auxiliary sequence

TheoremShakov's sequence counts the divisors of \(m^2 + 1\)#●ready to prove

Let \(s\) be Shakov's \(2\)-regular sequence and let \(\tau(N)\) denote the number of positive divisors of \(N\). Then \(s(n) \ge 0\) for every \(n \ge 1\), and for every natural number \(m\) the set \(\{n \ge 1 : s(n) = m\}\) is finite and has exactly \(\tau(m^2 + 1)\) elements.

This is the coefficientwise form of the identity \(\sum_{m \ge 0} \tau(m^2 + 1) x^m = \sum_{n \ge 1} x^{s(n)}\) of formal power series.

theorem_wanted fiber_card (m : ℕ) :
    (∀ n : ℕ, 1 ≤ n → 0 ≤ shakovSeq n) ∧
      ∃ F : Finset ℕ,
        (∀ n : ℕ, n ∈ F ↔ 1 ≤ n ∧ shakovSeq n = (m : ℤ)) ∧
          F.card = (m ^ 2 + 1).divisors.card

Sources

• Anton Shakov, "A 2-Regular Sequence That Counts The Divisors of n^2 + 1", Theorem 4.

Uses 1

Statement usesShakov's \(2\)-regular sequence

TheoremBlock averages of Shakov's sequence#●ready to prove

Let \(s\) be Shakov's \(2\)-regular sequence. For every natural number \(n\),

\[ \frac{1}{2^n} \sum_{2^n \le t < 2^{n+1}} s(t) = \frac{(5 + \sqrt{17})^n - (5 - \sqrt{17})^n}{2^{2n-1} \sqrt{17}}, \]

where the exponent \(2n - 1\) is read as \(0\) when \(n = 0\) (both sides are then \(0\)).

theorem_wanted block_average (n : ℕ) :
    (1 / (2 : ℝ) ^ n) *
        (∑ t ∈ Finset.Ico (2 ^ n) (2 ^ (n + 1)),
          (shakovSeq t : ℝ)) =
      ((5 + Real.sqrt 17) ^ n - (5 - Real.sqrt 17) ^ n) /
        ((2 : ℝ) ^ (2 * n - 1) * Real.sqrt 17)

Sources

• Anton Shakov, "A 2-Regular Sequence That Counts The Divisors of n^2 + 1", Proposition 7.

Uses 1

Statement usesShakov's \(2\)-regular sequence

TheoremPrimality of \(n^2 + 1\) from the fibers of Shakov's sequence#●ready to prove

Let \(s\) be Shakov's \(2\)-regular sequence. For every natural number \(n \ge 1\), the number \(n^2 + 1\) is prime if and only if the set of natural numbers \(m\) with \(s(m) = n\) is exactly \(\{2^n, 2^{n+1} - 1\}\).

theorem_wanted prime_iff_fiber (n : ℕ) (hn : 1 ≤ n) :
    Nat.Prime (n ^ 2 + 1) ↔
      {m : ℕ | shakovSeq m = (n : ℤ)} = {2 ^ n, 2 ^ (n + 1) - 1}

Sources

• Anton Shakov, "A 2-Regular Sequence That Counts The Divisors of n^2 + 1", Proposition 8.

Uses 1

Statement usesShakov's \(2\)-regular sequence

TheoremShakov's sequence takes Fibonacci values along the auxiliary sequence#●ready to prove

Let \(s\) be Shakov's \(2\)-regular sequence, let \(a\) be Shakov's auxiliary sequence, and let \(F_k\) denote the \(k\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\). For every natural number \(n \ge 1\), \(s(\max(a(n), 0)) = F_{n-1}\).

The source shows that \(a(n)\) is a positive integer and numbers the Fibonacci numbers so that this reads \(s(a(n)) = F_n\).

theorem_wanted shakovSeq_shakovA (n : ℕ) (hn : 1 ≤ n) :
    shakovSeq (shakovA n).toNat = (Nat.fib (n - 1) : ℤ)

Sources

• Anton Shakov, "A 2-Regular Sequence That Counts The Divisors of n^2 + 1", Proposition 9.

Uses 2

Statement usesShakov's auxiliary sequence · Shakov's \(2\)-regular sequence

TheoremFibonacci squares plus one are eventually composite#●ready to prove

Let \(F_k\) denote the \(k\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\). For every natural number \(k \ge 4\), the number \(F_k^2 + 1\) is composite.

In the source's numbering of the Fibonacci numbers, which is shifted by one, this reads "\(F_n^2 + 1\) is composite for \(n > 4\)".

theorem_wanted fib_sq_add_one_composite (k : ℕ) (hk : 4 ≤ k) :
    Nat.IsComposite (Nat.fib k ^ 2 + 1)

Sources

• Anton Shakov, "A 2-Regular Sequence That Counts The Divisors of n^2 + 1", Corollary 10.

Uses 1

Statement usesComposite numbers

2 fully proved5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.