Kolakoski sequence

DefinitionStarting positions of Kolakoski blocks#✓fully proved

For a sequence \(K_1, K_2, K_3, \ldots\) of natural numbers, the starting positions \(s_n\) of its blocks are defined by \(s_1 = 1\) and \(s_{n+1} = s_n + K_n\) for every \(n \ge 1\), together with the convention \(s_0 = 0\).

Block \(n\) of a candidate Kolakoski sequence \(K\) consists of the positions \(i\) with \(s_n \le i < s_n + K_n\); index \(0\) lies outside the one-indexed sequence.

def kolakoskiBlockStart (K : ℕ → ℕ) : ℕ → ℕ
  | 0 => 0
  | 1 => 1
  | n + 2 => kolakoskiBlockStart K (n + 1) + K (n + 1)

Used by 1

Used byKolakoski sequences

DefinitionKolakoski sequences#✓fully proved

A sequence \(K_1, K_2, K_3, \ldots\) of natural numbers is a Kolakoski sequence when \(K_1 = 1\), every \(K_n\) with \(n \ge 1\) is \(1\) or \(2\), and \(K\) describes its own runs in the following sense. Let \(s_1 = 1\) and \(s_{n+1} = s_n + K_n\) for \(n \ge 1\), and call block \(n\) the set of positions \(i\) with \(s_n \le i < s_n + K_n\). For every \(n \ge 1\), every term \(K_i\) with \(i\) in block \(n\) equals \(1\) if \(n\) is odd and \(2\) if \(n\) is even.

The sequence is indexed from \(1\); its value at index \(0\) is unconstrained.

def IsKolakoski (K : ℕ → ℕ) : Prop :=
  K 1 = 1 ∧
    (∀ n : ℕ, 1 ≤ n → K n = 1 ∨ K n = 2) ∧
    ∀ n : ℕ, 1 ≤ n → ∀ i : ℕ,
      kolakoskiBlockStart K n ≤ i →
      i < kolakoskiBlockStart K n + K n →
      K i = if n % 2 = 1 then 1 else 2

Uses 1

Statement usesStarting positions of Kolakoski blocks

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.