Tribonacci word

InductiveThe Tribonacci alphabet#✓fully proved

The Tribonacci word is written over the three-letter alphabet whose letters are \(a\), \(b\) and \(c\).

inductive TribonacciLetter : Type
  | a : TribonacciLetter
  | b : TribonacciLetter
  | c : TribonacciLetter
  deriving DecidableEq, Repr, Inhabited

Used by 12

Used byDuchêne–Rigo: letters of the Tribonacci word from Tribonacci representations · Gaps in the first column of the Trithoff array · Wall, seed and pre-seed of the Trithoff array via the Tribonacci word · The infinite Tribonacci word · Finite Tribonacci words · Recursion for the finite Tribonacci words · Length recurrence for finite Tribonacci words · Length lower bound for finite Tribonacci words · Lengths of finite Tribonacci words are monotone · Finite Tribonacci words form a prefix chain · Each finite Tribonacci word is a prefix of the next · Finite Tribonacci words agree with the infinite word

DefinitionFinite Tribonacci words#✓fully proved

The finite Tribonacci words \(W(n)\), for \(n \ge 0\), are the words over the alphabet \(\{a, b, c\}\) defined by \(W(0) = a\), \(W(1) = ab\), \(W(2) = abac\) and \(W(n + 3) = W(n + 2)\,W(n + 1)\,W(n)\) for every \(n \ge 0\), where juxtaposition denotes concatenation.

def tribonacciWordApprox : Nat → List TribonacciLetter
  | 0 => [.a]
  | 1 => [.a, .b]
  | 2 => [.a, .b, .a, .c]
  | n + 3 => tribonacciWordApprox (n + 2) ++ tribonacciWordApprox (n + 1) ++
      tribonacciWordApprox n

Uses 1 · Used by 8

Statement usesThe Tribonacci alphabet

Used byThe infinite Tribonacci word · Recursion for the finite Tribonacci words · Length recurrence for finite Tribonacci words · Length lower bound for finite Tribonacci words · Lengths of finite Tribonacci words are monotone · Finite Tribonacci words form a prefix chain · Each finite Tribonacci word is a prefix of the next · Finite Tribonacci words agree with the infinite word

TheoremRecursion for the finite Tribonacci words#✓fully proved

For every \(n \ge 0\), the finite Tribonacci word \(W(n + 3)\) is the concatenation \(W(n + 2)\,W(n + 1)\,W(n)\).

theorem tribonacciWordApprox_add_three (n : Nat) :
    tribonacciWordApprox (n + 3) =
      tribonacciWordApprox (n + 2) ++ tribonacciWordApprox (n + 1) ++
        tribonacciWordApprox n

Uses 2 · Used by 1

Statement usesThe Tribonacci alphabet · Finite Tribonacci words

Used byEach finite Tribonacci word is a prefix of the next

TheoremLength recurrence for finite Tribonacci words#✓fully proved

Writing \(|w|\) for the length of a word \(w\), for every \(n \ge 0\) the finite Tribonacci words satisfy \(|W(n + 3)| = |W(n + 2)| + |W(n + 1)| + |W(n)|\).

theorem tribonacciWordApprox_length_add_three (n : Nat) :
    (tribonacciWordApprox (n + 3)).length =
      (tribonacciWordApprox (n + 2)).length +
        (tribonacciWordApprox (n + 1)).length + (tribonacciWordApprox n).length

Uses 2 · Used by 1

Statement usesThe Tribonacci alphabet · Finite Tribonacci words

Used byLength lower bound for finite Tribonacci words

TheoremLength lower bound for finite Tribonacci words#✓fully proved

For every \(n \ge 0\), the finite Tribonacci word \(W(n)\) has length at least \(n + 1\).

theorem tribonacciWordApprox_length_ge (n : Nat) :
    n + 1 ≤ (tribonacciWordApprox n).length

Uses 3 · Used by 2

Statement usesThe Tribonacci alphabet · Finite Tribonacci words

Proof usesLength recurrence for finite Tribonacci words

Used byThe infinite Tribonacci word · Finite Tribonacci words agree with the infinite word

TheoremEach finite Tribonacci word is a prefix of the next#✓fully proved

For every \(n \ge 0\), the finite Tribonacci word \(W(n)\) is a prefix of \(W(n + 1)\).

theorem tribonacciWordApprox_prefix_succ : ∀ n : Nat,
    List.IsPrefix (tribonacciWordApprox n) (tribonacciWordApprox (n + 1))

Uses 3 · Used by 1

Statement usesThe Tribonacci alphabet · Finite Tribonacci words

Proof usesRecursion for the finite Tribonacci words

Used byFinite Tribonacci words form a prefix chain

TheoremFinite Tribonacci words form a prefix chain#✓fully proved

For all natural numbers \(m \le n\), the finite Tribonacci word \(W(m)\) is a prefix of \(W(n)\).

theorem tribonacciWordApprox_prefix {m n : Nat} (h : m ≤ n) :
    List.IsPrefix (tribonacciWordApprox m) (tribonacciWordApprox n)

Uses 3 · Used by 2

Statement usesThe Tribonacci alphabet · Finite Tribonacci words

Proof usesEach finite Tribonacci word is a prefix of the next

Used byLengths of finite Tribonacci words are monotone · Finite Tribonacci words agree with the infinite word

TheoremLengths of finite Tribonacci words are monotone#✓fully proved

For all natural numbers \(m \le n\), the length of the finite Tribonacci word \(W(m)\) is at most the length of \(W(n)\).

theorem tribonacciWordApprox_length_mono {m n : Nat} (h : m ≤ n) :
    (tribonacciWordApprox m).length ≤ (tribonacciWordApprox n).length

Uses 3

Statement usesThe Tribonacci alphabet · Finite Tribonacci words

Proof usesFinite Tribonacci words form a prefix chain

DefinitionThe infinite Tribonacci word#✓fully proved

The infinite Tribonacci word is the sequence over the alphabet \(\{a, b, c\}\) whose letter at each position \(k \ge 0\) (positions counted from \(0\)) is the letter at position \(k\) of the finite Tribonacci word \(W(k)\); this position exists because \(W(k)\) has length at least \(k + 1\).

def tribonacciWord (k : Nat) : TribonacciLetter :=
  (tribonacciWordApprox k)[k]'(by
    have h := tribonacciWordApprox_length_ge k
    omega)

Uses 3 · Used by 4

Statement usesThe Tribonacci alphabet · Finite Tribonacci words · Length lower bound for finite Tribonacci words

Used byDuchêne–Rigo: letters of the Tribonacci word from Tribonacci representations · Gaps in the first column of the Trithoff array · Wall, seed and pre-seed of the Trithoff array via the Tribonacci word · Finite Tribonacci words agree with the infinite word

TheoremFinite Tribonacci words agree with the infinite word#✓fully proved

For all natural numbers \(k \le n\) such that \(k\) is less than the length of the finite Tribonacci word \(W(n)\), the letter of \(W(n)\) at position \(k\) equals the letter of the infinite Tribonacci word at position \(k\), positions being counted from \(0\).

theorem tribonacciWord_eq_getElem_of_le (k n : Nat) (hkn : k ≤ n)
    (hk : k < (tribonacciWordApprox n).length) :
    (tribonacciWordApprox n)[k]'hk = tribonacciWord k

Uses 5

Statement usesThe Tribonacci alphabet · The infinite Tribonacci word · Finite Tribonacci words

Proof usesLength lower bound for finite Tribonacci words · Finite Tribonacci words form a prefix chain

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.