Thue–Morse sequence and its generalizations

DefinitionCyclic letter shift#✓fully proved

For \(L \in \mathbb{N}\) and letters \(a, t\) of the alphabet \(\{0, \dots, L-1\}\), the cyclic shift of \(a\) by \(t\) is the letter \((a + t) \bmod L\). Writing the letters as \(a_0, \dots, a_{L-1}\), it sends \(a_i\) to \(a_{(i + t) \bmod L}\).

public def shiftLetter {L : Nat} (a t : Fin L) : Fin L :=
  ⟨(a.val + t.val) % L, Nat.mod_lt _ (Nat.lt_of_le_of_lt (Nat.zero_le _) a.2)⟩

Sources

• JIS Definition 2.2.

Used by 4

Used byValue of the cyclic letter shift · Cyclic shift of a word · Cyclic shifting preserves word length · Letters of a cyclically shifted word

DefinitionCyclic shift of a word#✓fully proved

Let \(L\) be a natural number and let \(t\) be a letter of the alphabet \(\{0, 1, \dots, L - 1\}\). The cyclic shift by \(t\) of a word \(w = a_1 a_2 \cdots a_n\) over this alphabet is the word \(\sigma_t(a_1) \sigma_t(a_2) \cdots \sigma_t(a_n)\) of the same length, where \(\sigma_t(a) = (a + t) \bmod L\) is the cyclic shift of a letter.

public def shiftWord {L : Nat} (t : Fin L) (w : List (Fin L)) : List (Fin L) :=
  List.map (fun a => shiftLetter a t) w

Uses 1 · Used by 5

Statement usesCyclic letter shift

Used byBlocks of the generalized Thue–Morse sequence · Length of the generalized Thue–Morse blocks · Each generalized Thue–Morse block is a prefix of the next · Cyclic shifting preserves word length · Letters of a cyclically shifted word

TheoremLetters of a cyclically shifted word#✓fully proved

Let \(L\) be a natural number and let \(t\) and \(b\) be letters of the alphabet \(\{0, 1, \dots, L - 1\}\). For a letter \(a\) write \(\sigma_t(a) = (a + t) \bmod L\) for its cyclic shift by \(t\), and for a word \(w\) over this alphabet write \(\sigma_t(w)\) for the word obtained by shifting each letter of \(w\). Then \(b\) occurs in \(\sigma_t(w)\) if and only if \(b = \sigma_t(a)\) for some letter \(a\) occurring in \(w\).

public theorem shiftWord_mem {L : Nat} (t : Fin L) (w : List (Fin L)) (b : Fin L) :
    b ∈ shiftWord t w ↔ ∃ a ∈ w, shiftLetter a t = b

Uses 2

Statement usesCyclic letter shift · Cyclic shift of a word

TheoremCyclic shifting preserves word length#✓fully proved

For every \(L \in \mathbb{N}\), every letter \(t\) of the alphabet \(\{0, \dots, L-1\}\) and every finite word \(w\) over that alphabet, the word obtained from \(w\) by shifting each letter cyclically by \(t\) has the same length as \(w\).

public theorem shiftWord_length {L : Nat} (t : Fin L) (w : List (Fin L)) :
    (shiftWord t w).length = w.length

Sources

• JIS Definition 2.2.

Uses 2 · Used by 1

Statement usesCyclic shift of a word

Proof usesCyclic letter shift

Used byLength of the generalized Thue–Morse blocks

TheoremValue of the cyclic letter shift#✓fully proved

For every \(L \in \mathbb{N}\) and all letters \(a, t\) of the alphabet \(\{0, \dots, L-1\}\), the cyclic shift of \(a\) by \(t\) is the letter \((a + t) \bmod L\).

public theorem shiftLetter_val {L : Nat} (a t : Fin L) :
    (shiftLetter a t).val = (a.val + t.val) % L

Sources

• JIS Definition 2.2.

Uses 1

Statement usesCyclic letter shift

DefinitionBlocks of the generalized Thue–Morse sequence#✓fully proved

Let \(L > 1\) and \(k > 1\) be natural numbers, take the letters \(0, 1, \dots, L-1\) (the elements of \(\mathbb{Z}/L\mathbb{Z}\)), and let \(\kappa\) assign a shift \(\kappa(j, n) \in \mathbb{Z}/L\mathbb{Z}\) to each \(j \in \{1, \dots, k-1\}\) and each \(n \ge 0\). For a word \(w\) and \(t \in \mathbb{Z}/L\mathbb{Z}\), let \(f^t(w)\) be the word obtained from \(w\) by adding \(t\) modulo \(L\) to every letter. The blocks \(A_n\) of the \((L, k, \kappa)\)-Thue–Morse sequence are the words given by \(A_0 = 0\) (a word of one letter) and \(A_{n+1} = A_n \, f^{\kappa(1, n)}(A_n) \, f^{\kappa(2, n)}(A_n) \cdots f^{\kappa(k-1, n)}(A_n)\).

public def block (L k : Nat) (hL : 1 < L) (hk : 1 < k)
    (kappa : Fin (k - 1) → Nat → Fin L) : Nat → List (Fin L)
  | 0 => [⟨0, by omega⟩]
  | n + 1 =>
    let prev := block L k hL hk kappa n
    prev ++ List.flatten (List.map (fun j => shiftWord (kappa j n) prev) (List.finRange (k - 1)))

Uses 1 · Used by 6

Statement usesCyclic shift of a word

Used byLength of the generalized Thue–Morse blocks · The generalized Thue–Morse blocks form a chain of prefixes · Each generalized Thue–Morse block is a prefix of the next · Classical Thue–Morse blocks · The infinite generalized Thue–Morse word · Later blocks agree with the infinite word

TheoremLength of a concatenation of equal-length lists#✓fully proved

Let \(l\) be a list of lists over a type and let \(m \in \mathbb{N}\). If every list in \(l\) has length \(m\), then the concatenation of the lists in \(l\) has length \(n \cdot m\), where \(n\) is the number of lists in \(l\).

public theorem length_flatten_eq {α : Type} (l : List (List α)) (m : Nat)
    (h : ∀ x ∈ l, x.length = m) : l.flatten.length = l.length * m

Sources

• JIS Definition 2.2.

Used by 1

Used byLength of the generalized Thue–Morse blocks

TheoremLength of the generalized Thue–Morse blocks#✓fully proved

Let \(L > 1\) and \(k > 1\) be natural numbers and let \(\kappa\) assign a shift \(\kappa(j, n) \in \mathbb{Z}/L\mathbb{Z}\) to each \(j \in \{1, \dots, k-1\}\) and each \(n \ge 0\). For every \(n \ge 0\), the block \(A_n\) of the \((L, k, \kappa)\)-Thue–Morse sequence has exactly \(k^n\) letters.

public theorem block_length (L k : Nat) (hL : 1 < L) (hk : 1 < k)
    (kappa : Fin (k - 1) → Nat → Fin L) (n : Nat) :
    (block L k hL hk kappa n).length = k ^ n

Uses 4 · Used by 3

Statement usesBlocks of the generalized Thue–Morse sequence

Proof usesLength of a concatenation of equal-length lists · Cyclic shift of a word · Cyclic shifting preserves word length

Used byLength of the classical Thue–Morse blocks · The infinite generalized Thue–Morse word · Later blocks agree with the infinite word

TheoremEach generalized Thue–Morse block is a prefix of the next#✓fully proved

Let \(L > 1\) and \(k > 1\) be natural numbers and let \(\kappa\) assign a shift \(\kappa(j, n) \in \mathbb{Z}/L\mathbb{Z}\) to each \(j \in \{1, \dots, k-1\}\) and each \(n \ge 0\). For every \(n \ge 0\), the block \(A_n\) of the \((L, k, \kappa)\)-Thue–Morse sequence is a prefix of \(A_{n+1}\): there is a word \(w\) with \(A_{n+1} = A_n w\).

public theorem block_prefix_succ (L k : Nat) (hL : 1 < L) (hk : 1 < k)
    (kappa : Fin (k - 1) → Nat → Fin L) (n : Nat) :
    ∃ tail, block L k hL hk kappa (n + 1) = block L k hL hk kappa n ++ tail

Uses 2 · Used by 1

Statement usesBlocks of the generalized Thue–Morse sequence

Proof usesCyclic shift of a word

Used byThe generalized Thue–Morse blocks form a chain of prefixes

TheoremThe generalized Thue–Morse blocks form a chain of prefixes#✓fully proved

Let \(L > 1\) and \(k > 1\) be natural numbers and let \(\kappa\) assign a shift \(\kappa(j, n) \in \mathbb{Z}/L\mathbb{Z}\) to each \(j \in \{1, \dots, k-1\}\) and each \(n \ge 0\). For all natural numbers \(m \le n\), the block \(A_m\) of the \((L, k, \kappa)\)-Thue–Morse sequence is a prefix of \(A_n\): there is a word \(w\) with \(A_n = A_m w\).

public theorem block_prefix (L k : Nat) (hL : 1 < L) (hk : 1 < k)
    (kappa : Fin (k - 1) → Nat → Fin L) {m n : Nat} (h : m ≤ n) :
    ∃ tail, block L k hL hk kappa n = block L k hL hk kappa m ++ tail

Uses 2 · Used by 1

Statement usesBlocks of the generalized Thue–Morse sequence

Proof usesEach generalized Thue–Morse block is a prefix of the next

Used byLater blocks agree with the infinite word

TheoremA crude exponential bound#✓fully proved

For every natural number \(k > 1\) and every \(m \in \mathbb{N}\), we have \(m < k^{m+1}\).

public theorem lt_pow_succ_self {k : Nat} (hk : 1 < k) (m : Nat) : m < k ^ (m + 1)

Sources

• JIS Definition 2.2.

Used by 2

Used byThe infinite generalized Thue–Morse word · Later blocks agree with the infinite word

TheoremIndexing into a concatenation#✓fully proved

Let \(l_1\) and \(l_2\) be lists over a type, and let \(m\) be a natural number less than the length of \(l_1\). Then the entry at position \(m\) of the concatenation of \(l_1\) followed by \(l_2\) equals the entry at position \(m\) of \(l_1\) (positions start at \(0\)).

public theorem get_append_left {α : Type} (l₁ l₂ : List α) (m : Nat)
    (h : m < (l₁ ++ l₂).length) (hm : m < l₁.length) :
    (l₁ ++ l₂).get ⟨m, h⟩ = l₁.get ⟨m, hm⟩

Sources

• JIS Definition 2.2.

Used by 1

Used byLater blocks agree with the infinite word

DefinitionThe infinite generalized Thue–Morse word#✓fully proved

Let \(L, k \ge 2\), let \(\kappa : \{1, \dots, k-1\} \times \mathbb{N} \to \{0, \dots, L-1\}\) be a shift schedule, and let \(A_0, A_1, \dots\) be the blocks of the \((L, k, \kappa)\)-Thue–Morse sequence. The infinite word \(A_\infty\) over the alphabet \(\{0, \dots, L-1\}\) has, for every \(m \in \mathbb{N}\), as its letter at position \(m\) (positions start at \(0\)) the letter at position \(m\) of the block \(A_{m+1}\), which has \(k^{m+1} > m\) letters.

The letter is read by checked indexing, with no default letter.

public def infLetter (L k : Nat) (hL : 1 < L) (hk : 1 < k)
    (kappa : Fin (k - 1) → Nat → Fin L) (m : Nat) : Fin L :=
  (block L k hL hk kappa (m + 1)).get
    ⟨m, by
      rw [block_length]
      exact lt_pow_succ_self hk m⟩

Sources

• JIS Definition 2.2.

Uses 3 · Used by 2

Statement usesBlocks of the generalized Thue–Morse sequence · Length of the generalized Thue–Morse blocks · A crude exponential bound

Used byThe classical Thue–Morse word begins with 01101001 · Later blocks agree with the infinite word

TheoremLater blocks agree with the infinite word#✓fully proved

Let \(L, k \ge 2\), let \(\kappa : \{1, \dots, k-1\} \times \mathbb{N} \to \{0, \dots, L-1\}\) be a shift schedule, and let \(A_0, A_1, \dots\) be the blocks and \(A_\infty\) the infinite word of the \((L, k, \kappa)\)-Thue–Morse sequence. For all \(m, N \in \mathbb{N}\) with \(m + 1 \le N\) and \(m\) less than the length of \(A_N\), the letter at position \(m\) of \(A_N\) equals the letter at position \(m\) of \(A_\infty\) (positions start at \(0\)).

public theorem infLetter_coherence (L k : Nat) (hL : 1 < L) (hk : 1 < k)
    (kappa : Fin (k - 1) → Nat → Fin L) (m N : Nat) (hN : m + 1 ≤ N)
    (h : m < (block L k hL hk kappa N).length) :
    (block L k hL hk kappa N).get ⟨m, h⟩ = infLetter L k hL hk kappa m

Sources

• JIS Definition 2.2.

Uses 6

Statement usesBlocks of the generalized Thue–Morse sequence · The infinite generalized Thue–Morse word

Proof usesLength of the generalized Thue–Morse blocks · The generalized Thue–Morse blocks form a chain of prefixes · Indexing into a concatenation · A crude exponential bound

DefinitionClassical shift schedule#✓fully proved

The classical shift schedule is the map \(\kappa\) that assigns to the index \(j = 1\) and every \(n \in \mathbb{N}\) the letter \(\kappa(1, n) = 1\) of the alphabet \(\{0, 1\}\). It is the schedule of the classical Thue–Morse sequence, the \((L, k, \kappa)\)-Thue–Morse sequence with \(L = k = 2\).

public def classicalKappa : Fin (2 - 1) → Nat → Fin 2 := fun _ _ => ⟨1, by decide⟩

Sources

• the classical \((2, 2, 1)\) example after JIS Definition 2.2.

Used by 3

Used byClassical Thue–Morse blocks · The classical Thue–Morse word begins with 01101001 · Length of the classical Thue–Morse blocks

DefinitionClassical Thue–Morse blocks#✓fully proved

The classical Thue–Morse blocks are the blocks \(A_n\) of the \((2, 2, \kappa)\)-Thue–Morse sequence with \(\kappa(1, n) = 1\) for every \(n \ge 0\). Thus \(A_0\) is the one-letter word \(0\), and \(A_{n+1}\) is \(A_n\) followed by the word obtained from \(A_n\) by exchanging the letters \(0\) and \(1\).

public def classicalBlock : Nat → List (Fin 2) :=
  block 2 2 (by decide) (by decide) classicalKappa

Uses 2 · Used by 5

Statement usesBlocks of the generalized Thue–Morse sequence · Classical shift schedule

Used byClassical Thue–Morse block of order 0 · Classical Thue–Morse block of order 1 · Classical Thue–Morse block of order 2 · Classical Thue–Morse block of order 3 · Length of the classical Thue–Morse blocks

TheoremLength of the classical Thue–Morse blocks#✓fully proved

For every \(n \in \mathbb{N}\), the classical Thue–Morse block \(A_n\) (the block \(A_n\) of the \((L, k, \kappa)\)-Thue–Morse sequence with \(L = k = 2\) and \(\kappa(1, i) = 1\) for all \(i \in \mathbb{N}\)) has exactly \(2^n\) letters.

public theorem classical_length (n : Nat) : (classicalBlock n).length = 2 ^ n

Sources

• the classical \((2, 2, 1)\) example after JIS Definition 2.2.

Uses 3

Statement usesClassical Thue–Morse blocks

Proof usesLength of the generalized Thue–Morse blocks · Classical shift schedule

TheoremClassical Thue–Morse block of order 0#✓fully proved

The classical Thue–Morse block \(A_0\) is the one-letter word \(0\).

public theorem classical_A0 : classicalBlock 0 = [⟨0, by decide⟩]

Uses 1

Statement usesClassical Thue–Morse blocks

TheoremClassical Thue–Morse block of order 1#✓fully proved

The classical Thue–Morse block \(A_1\) is the word \(01\).

public theorem classical_A1 : classicalBlock 1 = [⟨0, by decide⟩, ⟨1, by decide⟩]

Uses 1

Statement usesClassical Thue–Morse blocks

TheoremClassical Thue–Morse block of order 2#✓fully proved

The classical Thue–Morse block \(A_2\) is the word \(0110\).

public theorem classical_A2 : classicalBlock 2 =
    [⟨0, by decide⟩, ⟨1, by decide⟩, ⟨1, by decide⟩, ⟨0, by decide⟩]

Uses 1

Statement usesClassical Thue–Morse blocks

TheoremClassical Thue–Morse block of order 3#✓fully proved

The classical Thue–Morse block \(A_3\) is the word \(01101001\).

public theorem classical_A3 : classicalBlock 3 =
    [⟨0, by decide⟩, ⟨1, by decide⟩, ⟨1, by decide⟩, ⟨0, by decide⟩,
     ⟨1, by decide⟩, ⟨0, by decide⟩, ⟨0, by decide⟩, ⟨1, by decide⟩]

Uses 1

Statement usesClassical Thue–Morse blocks

TheoremThe classical Thue–Morse word begins with 01101001#✓fully proved

Let \(A_\infty\) be the infinite word of the \((2, 2, \kappa)\)-Thue–Morse sequence with \(\kappa(1, n) = 1\) for every \(n \ge 0\). The letters of \(A_\infty\) at positions \(0, 1, \dots, 7\) are \(0, 1, 1, 0, 1, 0, 0, 1\), so \(A_\infty\) begins with \(01101001\).

public theorem classical_inf_init :
    infLetter 2 2 (by decide) (by decide) classicalKappa 0 = ⟨0, by decide⟩ ∧
    infLetter 2 2 (by decide) (by decide) classicalKappa 1 = ⟨1, by decide⟩ ∧
    infLetter 2 2 (by decide) (by decide) classicalKappa 2 = ⟨1, by decide⟩ ∧
    infLetter 2 2 (by decide) (by decide) classicalKappa 3 = ⟨0, by decide⟩ ∧
    infLetter 2 2 (by decide) (by decide) classicalKappa 4 = ⟨1, by decide⟩ ∧
    infLetter 2 2 (by decide) (by decide) classicalKappa 5 = ⟨0, by decide⟩ ∧
    infLetter 2 2 (by decide) (by decide) classicalKappa 6 = ⟨0, by decide⟩ ∧
    infLetter 2 2 (by decide) (by decide) classicalKappa 7 = ⟨1, by decide⟩

Uses 2

Statement usesClassical shift schedule · The infinite generalized Thue–Morse word

DefinitionThue–Morse substitution#✓fully proved

The Thue–Morse substitution \(\sigma\) on the alphabet \(\{0, 1\}\) sends each letter to a word of length two: \(\sigma(0) = 01\) and \(\sigma(1) = 10\).

def thueMorseSubstitution : Bool → List Bool
  | false => [false, true]
  | true => [true, false]

Sources

• Example 2 in Scott Balchin and Dan Rust, Computations for Symbolic Substitutions, Journal of Integer Sequences 20 (2017): https://cs.uwaterloo.ca/journals/JIS/VOL20/Rust/rust3.tex.

Used by 2

Used byExtension of the Thue–Morse substitution to binary words · Thue–Morse blocks

DefinitionThue–Morse blocks#✓fully proved

Let \(\sigma\) be the Thue–Morse substitution, \(\sigma(0) = 01\) and \(\sigma(1) = 10\), applied to finite words over \(\{0, 1\}\) letter by letter. For a natural number \(n\), the \(n\)th Thue–Morse block is the finite word \(\sigma^n(0)\): the \(0\)th block is the one-letter word \(0\), and the \((n+1)\)st block is obtained from the \(n\)th by replacing each letter \(a\) with \(\sigma(a)\).

def thueMorseBlock : Nat → List Bool
  | 0 => [false]
  | n + 1 => (thueMorseBlock n).flatMap thueMorseSubstitution

Uses 1

Statement usesThue–Morse substitution

DefinitionThue–Morse sequence#✓fully proved

The Thue–Morse sequence \(t_0 t_1 t_2 \cdots\) over \(\{0, 1\}\) is indexed from \(0\), and \(t_n = 1\) exactly when the binary expansion of \(n\) has an odd number of digits equal to \(1\); otherwise \(t_n = 0\).

def thueMorse (n : Nat) : Bool :=
  decide ((Nat.digits 2 n).count 1 % 2 = 1)

Sources

• Eiji Miyanohara, Transcendence of Digital Expansions Generated by a Generalized Thue-Morse Sequence, Journal of Integer Sequences 18 (2015), which lists the initial blocks 0, 01, 0110 and 01101001 and the limit beginning 0110100110010110: https://cs.uwaterloo.ca/journals/JIS/VOL18/Miyanohara/miy5.tex. Evaluation here uses the binary digits of the index, in time and space logarithmic in it, rather than an exponentially long block.

Used by 13

Used by\(\mathcal{M}_2\) is the Thue–Morse sequence along a binary digit mask · Factors of the Thue–Morse word are closed under complement · Factor complexity of the Thue–Morse Quarto word versus Thue–Morse · Factor complexity of the Thue–Morse Quarto word at powers of two · Thue–Morse quarto sequence from the Thue–Morse sequence · Maximum number of alternations in Thue–Morse factors · Minimum number of alternations in Thue–Morse factors · Reduced complexity of the Thue–Morse word at even lengths · Reduced complexity of the Thue–Morse word at odd lengths · Characterization of the Thue–Morse word among words starting with \(abba\) · Characterization of the cloned Thue–Morse words by their relative positions · Characterization of the Thue–Morse word by its relative positions · Tóth's paperfolding and Thue–Morse series for \(\zeta(2k+1)\)

25 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.