Fibonacci word
DefinitionFibonacci substitution#✓fully proved
The Fibonacci substitution sends each letter of the binary alphabet \(\{0, 1\}\) to a finite binary word: it maps \(0\) to \(01\) and \(1\) to \(0\).
The letters \(0\) and \(1\) are represented by the Booleans false and true.
DefinitionFibonacci morphism#✓fully proved
The Fibonacci morphism \(\varphi\) extends the Fibonacci substitution \(\sigma\), which maps \(0\) to \(01\) and \(1\) to \(0\), to finite binary words by concatenation: \(\varphi\) maps the empty word to the empty word, and \(\varphi(bw) = \sigma(b)\varphi(w)\) for every letter \(b\) and every finite binary word \(w\).
def fibMorph : List Bool → List Bool
| [] => []
| b :: w => fibSubst b ++ fibMorph wdef fibSubst : Bool → List Bool
| false => [false, true]
| true => [false]MathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:20
Uses 1 · Used by 8
DefinitionFinite Fibonacci words#✓fully proved
The finite Fibonacci words \(f_n\), for natural numbers \(n\), are the words in the letters \(0\) and \(1\) defined by \(f_0 = 0\) and \(f_{n+1} = \varphi(f_n)\), where \(\varphi\) is the Fibonacci morphism, which replaces each letter \(0\) by \(01\) and each letter \(1\) by \(0\).
The first words are \(0\), \(01\), \(010\), \(01001\), \(01001010\), and so on.
def fibWord : ℕ → List Bool
| 0 => [false]
| n + 1 => fibMorph (fibWord n)def fibMorph : List Bool → List Bool
| [] => []
| b :: w => fibSubst b ++ fibMorph wMathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:26
Uses 1 · Used by 21
DefinitionInfinite Fibonacci word#✓fully proved
Let \(f_0 = 0\) and let \(f_{k+1}\) be the image of \(f_k\) under the Fibonacci morphism (\(0 \mapsto 01\), \(1 \mapsto 0\)), so that \(f_0, f_1, f_2, \ldots\) are the finite Fibonacci words \(0, 01, 010, 01001, \ldots\). The one-sided infinite Fibonacci word is the infinite binary word whose letter at index \(n\) (indices start at \(0\)) is the letter of \(f_{n+2}\) at index \(n\).
Each \(f_k\) is a prefix of \(f_{k+1}\) and \(f_{n+2}\) has more than \(n\) letters, so this word is the limit of the finite Fibonacci words.
def fibInf (n : ℕ) : Bool :=
(fibWord (n + 2)).getD n falsedef fibWord : ℕ → List Bool
| 0 => [false]
| n + 1 => fibMorph (fibWord n)MathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:33
Uses 1 · Used by 19
TheoremThe Fibonacci morphism respects concatenation#✓fully proved
Let \(\varphi\) be the Fibonacci morphism on finite binary words, induced by \(0 \mapsto 01\) and \(1 \mapsto 0\). For all finite binary words \(a\) and \(b\), \(\varphi(ab) = \varphi(a)\varphi(b)\), where juxtaposition denotes concatenation.
theorem fibMorph_append : ∀ (a b : List Bool), fibMorph (a ++ b) = fibMorph a ++ fibMorph bdef fibMorph : List Bool → List Bool
| [] => []
| b :: w => fibSubst b ++ fibMorph wMathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:26
Uses 2 · Used by 3
TheoremThe Fibonacci morphism does not shorten words#✓fully proved
Let \(\varphi\) be the Fibonacci morphism on finite binary words, induced by \(0 \mapsto 01\) and \(1 \mapsto 0\). For every finite binary word \(w\), the length of \(\varphi(w)\) is at least the length of \(w\), that is, \(|w| \le |\varphi(w)|\).
The reason is that every letter maps to a nonempty word.
theorem fibMorph_length_ge : ∀ (w : List Bool), w.length ≤ (fibMorph w).lengthdef fibMorph : List Bool → List Bool
| [] => []
| b :: w => fibSubst b ++ fibMorph wMathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:26
Uses 1 · Used by 1
TheoremFinite Fibonacci words begin with \(0\)#✓fully proved
Let \(f_0 = 0\) and let \(f_{k+1}\) be the image of \(f_k\) under the Fibonacci morphism (\(0 \mapsto 01\), \(1 \mapsto 0\)). For every natural number \(n\), there is a finite binary word \(t\) such that \(f_n = 0t\), that is, the first letter of \(f_n\) is \(0\).
theorem fibWord_head : ∀ (n : ℕ), ∃ t, fibWord n = false :: tdef fibWord : ℕ → List Bool
| 0 => [false]
| n + 1 => fibMorph (fibWord n)MathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:33
Uses 3 · Used by 1
TheoremLower bound on the length of the finite Fibonacci words#✓fully proved
Let \(f_0 = 0\) and let \(f_{k+1}\) be the image of \(f_k\) under the Fibonacci morphism (\(0 \mapsto 01\), \(1 \mapsto 0\)). For every natural number \(n\), the word \(f_n\) has length at least \(n + 1\).
theorem fibWord_length : ∀ (n : ℕ), n + 1 ≤ (fibWord n).lengthdef fibWord : ℕ → List Bool
| 0 => [false]
| n + 1 => fibMorph (fibWord n)MathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:33
Uses 5 · Used by 3
TheoremConsecutive finite Fibonacci words are nested#✓fully proved
For every natural number \(n\), the \(n\)-th finite Fibonacci word \(f_n\) is a prefix of \(f_{n+1}\): there is a finite word \(t\) in the letters \(0\) and \(1\) with \(f_{n+1} = f_n t\).
theorem fibWord_nested_succ : ∀ (n : ℕ), ∃ t, fibWord (n + 1) = fibWord n ++ tdef fibWord : ℕ → List Bool
| 0 => [false]
| n + 1 => fibMorph (fibWord n)MathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:33
Uses 3 · Used by 2
TheoremEarlier finite Fibonacci words are prefixes of later ones#✓fully proved
For all natural numbers \(n \le m\), the \(n\)-th finite Fibonacci word \(f_n\) is a prefix of the \(m\)-th finite Fibonacci word \(f_m\): there is a finite word \(t\) in the letters \(0\) and \(1\) with \(f_m = f_n t\).
theorem fibWord_prefix : ∀ (n m : ℕ), n ≤ m → ∃ t, fibWord m = fibWord n ++ tdef fibWord : ℕ → List Bool
| 0 => [false]
| n + 1 => fibMorph (fibWord n)MathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:33
Uses 2 · Used by 2
TheoremAppending a word does not change earlier letters#✓fully proved
Let \(a\) and \(t\) be finite words in the letters \(0\) and \(1\), and let \(k\) be a natural number smaller than the length of \(a\). Then the letter at position \(k\) of the concatenation \(a t\) equals the letter at position \(k\) of \(a\), counting positions from \(0\).
theorem getD_append_prefix : ∀ (a t : List Bool) (k : ℕ),
k < a.length → (a ++ t).getD k false = a.getD k falseUsed by 1
TheoremLetters of the finite Fibonacci words stabilize#✓fully proved
Let \(f_0 = 0\) and let \(f_{k+1}\) be the image of \(f_k\) under the Fibonacci morphism (\(0 \mapsto 01\), \(1 \mapsto 0\)). For all natural numbers \(n \le m\) and every index \(i\) less than the length of \(f_n\) (indices start at \(0\)), the letter of \(f_m\) at index \(i\) equals the letter of \(f_n\) at index \(i\).
theorem fibWord_getD_eq (n m k : ℕ) (hle : n ≤ m) (hk : k < (fibWord n).length) :
(fibWord m).getD k false = (fibWord n).getD k falsedef fibWord : ℕ → List Bool
| 0 => [false]
| n + 1 => fibMorph (fibWord n)MathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:33
Uses 3 · Used by 1
TheoremThe finite Fibonacci word of index \(n + 2\) has more than \(n\) letters#✓fully proved
Let \(f_0 = 0\) and let \(f_{k+1}\) be the image of \(f_k\) under the Fibonacci morphism (\(0 \mapsto 01\), \(1 \mapsto 0\)). For every natural number \(n\), the length of \(f_{n+2}\) is greater than \(n\).
theorem fibInf_bound (n : ℕ) : n < (fibWord (n + 2)).lengthdef fibWord : ℕ → List Bool
| 0 => [false]
| n + 1 => fibMorph (fibWord n)MathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:33
Uses 2 · Used by 1
TheoremFinite Fibonacci words agree with the infinite Fibonacci word#✓fully proved
Let \(f_0 = 0\) and let \(f_{k+1}\) be the image of \(f_k\) under the Fibonacci morphism (\(0 \mapsto 01\), \(1 \mapsto 0\)). For all natural numbers \(m\) and \(n\) such that \(n\) is less than the length of \(f_m\), the letter of \(f_m\) at index \(n\) equals the letter at index \(n\) of the one-sided infinite Fibonacci word (indices start at \(0\)). In other words, every \(f_m\) is a prefix of the infinite Fibonacci word.
theorem fibInf_agrees (m n : ℕ) (hm : n < (fibWord m).length) :
(fibWord m).getD n false = fibInf ndef fibWord : ℕ → List Bool
| 0 => [false]
| n + 1 => fibMorph (fibWord n)MathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:33
def fibInf (n : ℕ) : Bool :=
(fibWord (n + 2)).getD n falseMathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:41
Uses 4 · Used by 4
TheoremRecurrence for the finite Fibonacci words#✓fully proved
Let \(f_0, f_1, f_2, \ldots\) be the finite Fibonacci words. For every natural number \(n\), \(f_{n+2} = f_{n+1} f_n\), where juxtaposition denotes concatenation.
theorem fibWord_add_two (n : ℕ) : fibWord (n + 2) = fibWord (n + 1) ++ fibWord ndef fibWord : ℕ → List Bool
| 0 => [false]
| n + 1 => fibMorph (fibWord n)MathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:33
Uses 3 · Used by 3
TheoremConcatenating the finite Fibonacci words#✓fully proved
For every natural number \(N\), prepending the letters \(0\) and \(1\) to the concatenation \(f_0 f_1 \cdots f_{N-1}\) of the first \(N\) finite Fibonacci words gives \(f_{N+1}\): that is, \(0\,1\,f_0 f_1 \cdots f_{N-1} = f_{N+1}\), where the concatenation is empty when \(N = 0\).
theorem fibWord_factorization (N : ℕ) :
false :: true :: (List.range N).flatMap fibWord = fibWord (N + 1)def fibWord : ℕ → List Bool
| 0 => [false]
| n + 1 => fibMorph (fibWord n)MathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:33
Uses 2 · Used by 2
TheoremFinite Fibonacci words are prefixes of the infinite Fibonacci word#✓fully proved
For every natural number \(n\), the finite Fibonacci word \(f_n\) is the word formed by the first \(|f_n|\) letters of the infinite Fibonacci word.
theorem fibWord_eq_ofFn_fibInf (n : ℕ) :
fibWord n = List.ofFn (fun i : Fin (fibWord n).length => fibInf i)def fibWord : ℕ → List Bool
| 0 => [false]
| n + 1 => fibMorph (fibWord n)MathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:33
def fibInf (n : ℕ) : Bool :=
(fibWord (n + 2)).getD n falseMathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:41
Uses 3 · Used by 1
TheoremFactorization of the infinite Fibonacci word into finite Fibonacci words#✓fully proved
Let \(f\) be the infinite Fibonacci word and let \(f_0, f_1, f_2, \ldots\) be the finite Fibonacci words. For every natural number \(N\), the finite word \(w_N = 0\,1\,f_0 f_1 \cdots f_{N-1}\) (so \(w_0 = 01\)) consists of the first \(|w_N|\) letters of \(f\), and for every natural number \(k\) the first \(k\) letters of \(f\) form a prefix of \(w_N\) for some \(N\). In this sense \(f = 0 \cdot 1 \cdot f_0 \cdot f_1 \cdot f_2 \cdots\).
theorem fibInf_factorization :
(∀ N : ℕ,
let w := false :: true :: (List.range N).flatMap fibWord
w = List.ofFn (fun i : Fin w.length => fibInf i)) ∧
∀ k : ℕ, ∃ N : ℕ,
List.ofFn (fun i : Fin k => fibInf i) <+:
false :: true :: (List.range N).flatMap fibWorddef fibWord : ℕ → List Bool
| 0 => [false]
| n + 1 => fibMorph (fibWord n)MathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:33
def fibInf (n : ℕ) : Bool :=
(fibWord (n + 2)).getD n falseMathlibExt/Combinatorics/InfiniteWord/FibonacciWord.lean:41
Sources
- Gabriele Fici, "Factorizations of the Fibonacci Infinite Word", Journal of Integer Sequences 18 (2015), Article 15.9.3, equation
fibo.
TheoremThe infinite Fibonacci word as \(0\) followed by the finite Fibonacci words#✓fully proved
Let \(f\) be an infinite word over \(\{0, 1\}\) and let \(f_1, f_2, f_3, \ldots\) be finite words over \(\{0, 1\}\) with \(f_1 = 1\), \(f_2 = 0\) and \(f_{n+3} = f_{n+2} f_{n+1}\) for every natural number \(n\), such that for every natural number \(n\) the word \(f_{n+2}\) consists of the first \(|f_{n+2}|\) letters of \(f\). Then for every natural number \(N\) the word \(w_N = 0\,f_1 f_2 \cdots f_N\) (so \(w_0 = 0\)) consists of the first \(|w_N|\) letters of \(f\), and for every natural number \(k\) the first \(k\) letters of \(f\) form a prefix of \(w_N\) for some \(N\). In this sense \(f = 0 \cdot f_1 \cdot f_2 \cdot f_3 \cdots\).
MetaMathlibExt.fibonacci_infinite_word_factorization · 16 lines
theorem fibonacci_infinite_word_factorization
(f : ℕ → Fin 2)
(fibWord : ℕ → List (Fin 2))
(h_one : fibWord 1 = [1])
(h_two : fibWord 2 = [0])
(h_rec : ∀ n : ℕ, fibWord (n + 3) = fibWord (n + 2) ++ fibWord (n + 1))
(h_limit : ∀ n : ℕ,
fibWord (n + 2) =
List.ofFn (fun i : Fin (fibWord (n + 2)).length => f i)) :
(∀ N : ℕ,
let w := 0 :: (List.range N).flatMap (fun n => fibWord (n + 1))
w = List.ofFn (fun i : Fin w.length => f i)) ∧
∀ k : ℕ, ∃ N : ℕ,
List.IsPrefix
(List.ofFn (fun i : Fin k => f i))
(0 :: (List.range N).flatMap (fun n => fibWord (n + 1)))Sources
- Gabriele Fici, "Factorizations of the Fibonacci Infinite Word", Journal of Integer Sequences 18 (2015), Article 15.9.3, Proposition lines 188-195 (equation
fibo), https://cs.uwaterloo.ca/journals/JIS/VOL18/Fici/fici5.tex.
TheoremKimberling's set modulo 2 is the Fibonacci word#✓fully proved
Let \(K\) be the set of natural numbers obtained from \(1\) by finitely many applications of the maps \(x \mapsto 2x\) and \(x \mapsto 4x - 1\). Let \(S\) be a strictly increasing sequence of natural numbers whose set of values is \(K\), and let \(w\) be the binary sequence with \(w(n) = 1\) if \(S(n + 1)\) is odd and \(w(n) = 0\) if \(S(n + 1)\) is even. Let \(\varphi\) be the morphism of binary words with \(\varphi(0) = 01\) and \(\varphi(1) = 0\). Then for every \(k \ge 0\), the first \(|\varphi^k(0)|\) terms \(w(0) w(1) \cdots\) of \(w\) spell the word \(\varphi^k(0)\). In other words, \(S\) modulo \(2\) with its first term dropped is the infinite Fibonacci word.
The source gives a third proof of this theorem of Kimberling, via a transducer construction; Allouche and Shallit also reproved it.
theorem kimberling_set_mod_two_fibonacci_word
(K : Set ℕ)
(hK : K = { n | ∃ w : List Bool,
w.foldl (fun x b => bif b then 4 * x - 1 else 2 * x) 1 = n })
(S : ℕ → ℕ) (hS : StrictMono S ∧ Set.range S = K)
(w : ℕ → Bool) (hw : ∀ n, w n = decide (S (n + 1) % 2 = 1))
(φ : List Bool → List Bool)
(hφ : φ = List.flatMap (fun b => bif b then [false] else [false, true])) :
∀ k : ℕ,
List.ofFn (fun i : Fin (φ^[k] [false]).length => w ↑i) = φ^[k] [false]Sources
- Tomi Kärki, Anne Lacroix, and Michel Rigo, "On the Recognizability of Self-Generating Sets," Journal of Integer Sequences 13 (2010), Article 10.2.2, Theorem (section Kimberling set and the Fibonacci word, label secKF), lines 710–714, https://cs.uwaterloo.ca/journals/JIS/VOL13/Rigo/rigo6.tex
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.