Irvine's conjecture on Kimberling's word

DefinitionKimberling's morphism#✓fully proved

Kimberling's morphism \(h\) sends each letter of the alphabet \(\{0, 1\}\) to a finite word over \(\{0, 1\}\), by \(h(1) = 110\) and \(h(0) = 11\).

The letters \(0\) and \(1\) are represented by the Boolean values false and true.

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

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 1 and Section 2 (the morphism h).

Used by 3

Used byKimberling's blocks · Each Kimberling block is a prefix of the next · Lower bound on the length of the Kimberling blocks

DefinitionKimberling's blocks#✓fully proved

Let \(h\) be Kimberling's morphism on the alphabet \(\{0, 1\}\), given by \(h(1) = 110\) and \(h(0) = 11\) and extended to finite words by concatenation. For each natural number \(n\), the \(n\)-th Kimberling block is the finite word \(K_n = h^n(1)\), the \(n\)-th iterate of \(h\) applied to the one-letter word \(1\). Thus \(K_0 = 1\), \(K_1 = 110\) and \(K_2 = 11011011\).

public def kimberlingBlock (n : ℕ) : List Bool :=
  morphIterate kimberlingMorphism n [true]

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 2 (K_n = h^n(1)).

Uses 2 · Used by 10

Statement usesKimberling's morphism · Iterates of a letter map

Used byClosed form for Gutkovskiy's sequence · Recursive structure of Kimberling's blocks · The first Kimberling block · Kimberling's blocks form a prefix chain · Each Kimberling block is a prefix of the next · The second Kimberling block · Kimberling's word · Every Kimberling block is a prefix of Kimberling's word · Lengths with two right-special factors in Kimberling's word · Lower bound on the length of the Kimberling blocks

TheoremThe first Kimberling block#✓fully proved

For Kimberling's morphism \(h\) on \(\{0, 1\}\), given by \(h(1) = 110\) and \(h(0) = 11\), the block \(K_1 = h(1)\) is the word \(110\).

public theorem kimberlingBlock_one : kimberlingBlock 1 = [true, true, false]

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 2.

Uses 1

Statement usesKimberling's blocks

TheoremThe second Kimberling block#✓fully proved

For Kimberling's morphism \(h\) on \(\{0, 1\}\), given by \(h(1) = 110\) and \(h(0) = 11\), the block \(K_2 = h^2(1)\) is the word \(11011011\).

public theorem kimberlingBlock_two :
    kimberlingBlock 2 = [true, true, false, true, true, false, true, true]

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 2.

Uses 1

Statement usesKimberling's blocks

TheoremEach Kimberling block is a prefix of the next#✓fully proved

Let \(h\) be Kimberling's morphism on \(\{0, 1\}\), \(h(1) = 110\) and \(h(0) = 11\), and let \(K_n = h^n(1)\). Then for every \(n \ge 0\), the word \(K_n\) is a prefix of \(K_{n+1}\).

Indeed \(h(1) = 110\) begins with \(1\), so \(h^n(1)\) is a prefix of \(h^n(110) = h^{n+1}(1)\).

public theorem kimberlingBlock_prefix_succ (n : ℕ) :
    kimberlingBlock n <+: kimberlingBlock (n + 1)

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 2.

Uses 4 · Used by 1

Statement usesKimberling's blocks

Proof usesKimberling's morphism · Extension of a letter map to finite words · Extended letter maps preserve concatenation

Used byKimberling's blocks form a prefix chain

TheoremKimberling's blocks form a prefix chain#✓fully proved

Let \(h\) be Kimberling's morphism on \(\{0, 1\}\), \(h(1) = 110\) and \(h(0) = 11\), and let \(K_n = h^n(1)\). Then \(K_m\) is a prefix of \(K_n\) for all natural numbers \(m \le n\).

public theorem kimberlingBlock_prefix {m n : ℕ} (h : m ≤ n) :
    kimberlingBlock m <+: kimberlingBlock n

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 2.

Uses 2 · Used by 1

Statement usesKimberling's blocks

Proof usesEach Kimberling block is a prefix of the next

Used byEvery Kimberling block is a prefix of Kimberling's word

TheoremLower bound on the length of the Kimberling blocks#✓fully proved

Let \(h\) be Kimberling's morphism on the alphabet \(\{0, 1\}\), given by \(h(1) = 110\) and \(h(0) = 11\), and let \(K_n = h^n(1)\). For every natural number \(n\), the word \(K_n\) has length at least \(2^n\).

This holds because the image of each letter under \(h\) has length at least \(2\).

public theorem two_pow_le_length_kimberlingBlock (n : ℕ) :
    2 ^ n ≤ (kimberlingBlock n).length

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 2.

Uses 3 · Used by 1

Statement usesKimberling's blocks

Proof usesKimberling's morphism · Extension of a letter map to finite words

Used byEvery Kimberling block is a prefix of Kimberling's word

DefinitionKimberling's word#✓fully proved

Let \(K_n\) be the \(n\)-th Kimberling block, a finite word over \(\{0, 1\}\). Kimberling's word \(k = k_1 k_2 k_3 \cdots = 1101101111\cdots\) (OEIS A285431) is the infinite word over \(\{0, 1\}\) whose letter \(k_{i+1}\), for \(i \ge 0\), is the \((i+1)\)-th letter of \(K_m\), where \(m = \lfloor \log_2 i \rfloor + 1\) for \(i \ge 1\) and \(m = 1\) for \(i = 0\). The block \(K_m\) has length at least \(2^m > i\), so this letter exists.

Every block \(K_n\) is a prefix of \(k\), so \(k\) is the common extension of the blocks.

public def kimberlingWord (i : ℕ) : Bool :=
  (kimberlingBlock (Nat.log 2 i + 1)).getD i false

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 2 (the limit word k) and Section 5 (k'_n = k_{n+1}).

Uses 1 · Used by 11

Statement usesKimberling's blocks

Used byIrvine's conjecture for Gutkovskiy's sequence · Positions of the ones in Kimberling's word · Position of the first one in Kimberling's word · Every Kimberling block is a prefix of Kimberling's word · The 101st letter of Kimberling's word · The first letters of Kimberling's word · Positions of the zeros in Kimberling's word · The first zero of Kimberling's word · Factor complexity of Kimberling's word · Lengths with two right-special factors in Kimberling's word · Critical exponent of Kimberling's word

TheoremEvery Kimberling block is a prefix of Kimberling's word#✓fully proved

Let \(k = k_1 k_2 k_3 \cdots\) be Kimberling's word and \(K_n\) the \(n\)-th Kimberling block. For all natural numbers \(i\) and \(n\) with \(i < |K_n|\), the letter \(k_{i+1}\) equals the \((i+1)\)-th letter of \(K_n\).

public theorem kimberlingWord_eq_getD {i n : ℕ} (hi : i < (kimberlingBlock n).length) :
    kimberlingWord i = (kimberlingBlock n).getD i false

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 2.

Uses 4

Statement usesKimberling's blocks · Kimberling's word

Proof usesKimberling's blocks form a prefix chain · Lower bound on the length of the Kimberling blocks

TheoremThe first letters of Kimberling's word#✓fully proved

The first four letters of Kimberling's word \(k = k_1 k_2 k_3 \cdots\) are \(k_1 k_2 k_3 k_4 = 1101\).

public theorem kimberlingWord_initial :
    kimberlingWord 0 = true ∧ kimberlingWord 1 = true ∧ kimberlingWord 2 = false ∧
      kimberlingWord 3 = true

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Table 1.

Uses 1 · Used by 2

Statement usesKimberling's word

Used byPosition of the first one in Kimberling's word · The first zero of Kimberling's word

TheoremThe 101st letter of Kimberling's word#✓fully proved

The letter \(k_{101}\) of Kimberling's word \(k = k_1 k_2 k_3 \cdots\) is \(0\) (OEIS A285431).

public theorem kimberlingWord_hundred : kimberlingWord 100 = false

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 2.

Uses 1

Statement usesKimberling's word

DefinitionTable of Gutkovskiy's sequence#✓fully proved

The Gutkovskiy tables \(T_0, T_1, \dots\) are finite lists of natural numbers, indexed from \(0\), defined by \(T_0 = [0]\) and, for \(n \ge 0\), \(T_{n+1}\) is \(T_n\) with the entry \((n + 1) - T_n[\lfloor T_n[n]/2 \rfloor]\) appended at the end. Here \(T_n[j]\) is the entry of \(T_n\) at index \(j\), or \(0\) if \(T_n\) has fewer than \(j + 1\) entries, and the subtraction is truncated at \(0\).

\(T_n\) has \(n + 1\) entries and lists the terms \(g_0, \dots, g_n\) of Gutkovskiy's sequence, so each step reads only values already computed.

public def gutkovskiyTable : ℕ → Array ℕ
  | 0 => #[0]
  | n + 1 =>
    let a := gutkovskiyTable n
    a.push ((n + 1) - a.getD (a.getD n 0 / 2) 0)

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 1, Equation (1).

Used by 5

Used byEntries of the Gutkovskiy table · Gutkovskiy's sequence · Gutkovskiy's sequence is bounded by the index · Recurrence for Gutkovskiy's sequence · Number of entries of the Gutkovskiy table

DefinitionGutkovskiy's sequence#✓fully proved

Gutkovskiy's sequence (OEIS A286389) is the sequence of natural numbers \(g_0, g_1, \dots\) with \(g_0 = 0\) and \(g_n = n - g_{\lfloor g_{n-1}/2 \rfloor}\) for \(n \ge 1\) (subtraction of natural numbers, truncated at \(0\)).

Formally, \(g_n\) is defined as \(T_n[n]\), the entry at index \(n\) of the Gutkovskiy table \(T_n\), and the recurrence is proved from the table.

public def gutkovskiy (n : ℕ) : ℕ :=
  (gutkovskiyTable n).getD n 0

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 1, Equation (1).

Uses 1 · Used by 9

Statement usesTable of Gutkovskiy's sequence

Used byEntries of the Gutkovskiy table · Irvine's conjecture for Gutkovskiy's sequence · Closed form for Gutkovskiy's sequence · Gutkovskiy's sequence from its parities · Gutkovskiy's sequence at \(100\) · First terms of Gutkovskiy's sequence · Gutkovskiy's sequence is bounded by the index · Recurrence for Gutkovskiy's sequence · Gutkovskiy's sequence modulo 2 is generated by a morphism

TheoremNumber of entries of the Gutkovskiy table#✓fully proved

For every natural number \(n\), the Gutkovskiy table up to index \(n\), the array of the values \(g_0, \dots, g_n\) of Gutkovskiy's sequence, has exactly \(n + 1\) entries.

public theorem size_gutkovskiyTable (n : ℕ) : (gutkovskiyTable n).size = n + 1

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 1, Equation (1).

Uses 1 · Used by 3

Statement usesTable of Gutkovskiy's sequence

Used byEntries of the Gutkovskiy table · Gutkovskiy's sequence is bounded by the index · Recurrence for Gutkovskiy's sequence

TheoremEntries of the Gutkovskiy table#✓fully proved

For natural numbers \(k \le n\), the entry at index \(k\) (counting from \(0\)) of the Gutkovskiy table \(T_n\) is the term \(g_k\) of Gutkovskiy's sequence.

public theorem getD_gutkovskiyTable {k n : ℕ} (h : k ≤ n) :
    (gutkovskiyTable n).getD k 0 = gutkovskiy k

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 1, Equation (1).

Uses 3 · Used by 1

Statement usesGutkovskiy's sequence · Table of Gutkovskiy's sequence

Proof usesNumber of entries of the Gutkovskiy table

Used byRecurrence for Gutkovskiy's sequence

TheoremGutkovskiy's sequence is bounded by the index#✓fully proved

For every natural number \(n\), the term \(g_n\) of Gutkovskiy's sequence satisfies \(g_n \le n\).

public theorem gutkovskiy_le (n : ℕ) : gutkovskiy n ≤ n

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 1, Equation (1).

Uses 3 · Used by 1

Statement usesGutkovskiy's sequence

Proof usesTable of Gutkovskiy's sequence · Number of entries of the Gutkovskiy table

Used byRecurrence for Gutkovskiy's sequence

TheoremRecurrence for Gutkovskiy's sequence#✓fully proved

For every natural number \(n\), Gutkovskiy's sequence satisfies \(g_{n+1} = (n + 1) - g_{\lfloor g_n/2 \rfloor}\) (subtraction of natural numbers, truncated at \(0\)).

public theorem gutkovskiy_succ (n : ℕ) :
    gutkovskiy (n + 1) = (n + 1) - gutkovskiy (gutkovskiy n / 2)

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 1, Equation (1).

Uses 5 · Used by 1

Statement usesGutkovskiy's sequence

Proof usesEntries of the Gutkovskiy table · Table of Gutkovskiy's sequence · Gutkovskiy's sequence is bounded by the index · Number of entries of the Gutkovskiy table

Used byFirst terms of Gutkovskiy's sequence

TheoremFirst terms of Gutkovskiy's sequence#✓fully proved

The first four terms of Gutkovskiy's sequence are \(g_0 = 0\), \(g_1 = 1\), \(g_2 = 2\) and \(g_3 = 2\).

public theorem gutkovskiy_initial :
    gutkovskiy 0 = 0 ∧ gutkovskiy 1 = 1 ∧ gutkovskiy 2 = 2 ∧ gutkovskiy 3 = 2

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Table 1.

Uses 2

Statement usesGutkovskiy's sequence

Proof usesRecurrence for Gutkovskiy's sequence

TheoremGutkovskiy's sequence at \(100\)#✓fully proved

The term \(g_{100}\) of Gutkovskiy's sequence is \(74\), in agreement with OEIS A286389.

public theorem gutkovskiy_hundred : gutkovskiy 100 = 74

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 1, Equation (1).

Uses 1

Statement usesGutkovskiy's sequence

DefinitionPositions of the ones in Kimberling's word#✓fully proved

Let \(k = k_1 k_2 k_3 \cdots\) be Kimberling's word over \(\{0, 1\}\). For \(n \ge 1\), \(A_n\) is the position of the \(n\)-th \(1\) in \(k\), that is, the \(n\)-th smallest index \(j \ge 1\) with \(k_j = 1\); by convention \(A_0 = 0\).

public noncomputable def kimberlingOnePosition (n : ℕ) : ℕ :=
  if n = 0 then 0 else Nat.nth (fun i ↦ kimberlingWord i = true) (n - 1) + 1

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 8 (the sequence A_n).

Uses 1 · Used by 2

Statement usesKimberling's word

Used byPositions of ones at the positions of zeros in Kimberling's word · Position of the first one in Kimberling's word

DefinitionPositions of the zeros in Kimberling's word#✓fully proved

Let \(k = k_1 k_2 k_3 \cdots\) be Kimberling's word over \(\{0, 1\}\). For \(n \ge 1\), \(B_n\) is the position of the \(n\)-th \(0\) in \(k\), that is, the \(n\)-th smallest index \(j \ge 1\) with \(k_j = 0\); by convention \(B_0 = 0\).

public noncomputable def kimberlingZeroPosition (n : ℕ) : ℕ :=
  if n = 0 then 0 else Nat.nth (fun i ↦ kimberlingWord i = false) (n - 1) + 1

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Section 8 (the sequence B_n).

Uses 1 · Used by 2

Statement usesKimberling's word

Used byPositions of ones at the positions of zeros in Kimberling's word · The first zero of Kimberling's word

TheoremPosition of the first one in Kimberling's word#✓fully proved

The position \(A_1\) of the first \(1\) in Kimberling's word \(k = k_1 k_2 k_3 \cdots\), counted from \(1\), is \(A_1 = 1\).

public theorem kimberlingOnePosition_one : kimberlingOnePosition 1 = 1

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Table 3.

Uses 3

Statement usesPositions of the ones in Kimberling's word

Proof usesKimberling's word · The first letters of Kimberling's word

TheoremThe first zero of Kimberling's word#✓fully proved

Let \(B_n\) be the position of the \(n\)-th \(0\) in Kimberling's word \(k = k_1 k_2 k_3 \cdots\). Then \(B_1 = 3\): the first \(0\) of \(k\) is \(k_3\).

public theorem kimberlingZeroPosition_one : kimberlingZeroPosition 1 = 3

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Table 3.

Uses 3

Statement usesPositions of the zeros in Kimberling's word

Proof usesKimberling's word · The first letters of Kimberling's word

TheoremRecursive structure of Kimberling's blocks#●ready to prove

Let \(h\) be Kimberling's morphism on \(\{0, 1\}\), \(h(1) = 110\) and \(h(0) = 11\), and let \(K_n = h^n(1)\). Then for every \(n \ge 2\), \(K_n = K_{n-1} K_{n-1} K_{n-2} K_{n-2}\) (concatenation of words).

public theorem_wanted kimberlingBlock_eq_append {n : ℕ} (hn : 2 ≤ n) :
    kimberlingBlock n = kimberlingBlock (n - 1) ++ kimberlingBlock (n - 1) ++
      kimberlingBlock (n - 2) ++ kimberlingBlock (n - 2)

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Proposition 1.

Uses 1

Statement usesKimberling's blocks

TheoremIrvine's conjecture for Gutkovskiy's sequence#●ready to prove

Let \(g_0, g_1, \dots\) be Gutkovskiy's sequence and let \(k_1 k_2 k_3 \cdots\) be Kimberling's word, with its letters read as the numbers \(0\) and \(1\). Then \(g_n = k_1 + \dots + k_n\) for every \(n \ge 0\) (the empty sum when \(n = 0\)).

public theorem_wanted gutkovskiy_eq_sum_kimberlingWord (n : ℕ) :
    gutkovskiy n = ∑ i ∈ Finset.range n, (kimberlingWord i).toNat

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Theorem 1.

Uses 2

Statement usesGutkovskiy's sequence · Kimberling's word

TheoremClosed form for Gutkovskiy's sequence#●ready to prove

Let \(g_0, g_1, \dots\) be Gutkovskiy's sequence, let \(|K_i|\) be the length of the Kimberling block \(K_i\), and let \(\alpha = (\sqrt{3} - 1)/2\) and \(\beta = \sqrt{3}/3\). Let \(n\) be a natural number and let \(a_0, a_1, \dots, a_{m-1}\) be digits in \(\{0, 1, 2\}\) such that no two consecutive digits \(a_i, a_{i+1}\) are both \(2\) and \(n = \sum_{i < m} a_i |K_i|\). If \(m \ge 1\) and \(a_0 = 1\), then \(g_n = 2\lfloor \alpha n \rfloor + 1\); if \(m \ge 1\) and \(a_0 \in \{0, 2\}\), then \(g_n = 2\lfloor \alpha n + \beta \rfloor\).

Written most significant digit first, \(a_{m-1} \cdots a_1 a_0\) is a \(K\)-representation of \(n\) ending in the digit \(a_0\); leading zeros are allowed.

public theorem_wanted gutkovskiy_eq_two_mul_floor {n : ℕ} {a : List ℕ} (ha : ∀ d ∈ a, d ≤ 2)
    (h22 : ¬ [2, 2] <:+: a)
    (hn : (a.mapIdx fun i d ↦ d * (kimberlingBlock i).length).sum = n) :
    (a.head? = some 1 → (gutkovskiy n : ℤ) = 2 * ⌊(√3 - 1) / 2 * (n : ℝ)⌋ + 1) ∧
      (a.head? = some 0 ∨ a.head? = some 2 →
        (gutkovskiy n : ℤ) = 2 * ⌊(√3 - 1) / 2 * (n : ℝ) + √3 / 3⌋)

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Theorem 2.

Uses 2

Statement usesGutkovskiy's sequence · Kimberling's blocks

TheoremPositions of ones at the positions of zeros in Kimberling's word#●ready to prove

Let \(k = k_1 k_2 k_3 \cdots\) be Kimberling's word, and for \(n \ge 1\) let \(A_n\) and \(B_n\) be the positions (counted from \(1\)) of the \(n\)-th \(1\) and of the \(n\)-th \(0\) in \(k\). Then for every \(n \ge 1\), either \(A_{B_n} = A_n + B_n - 1\) or \(A_{B_n} = A_n + B_n\).

This answers a problem of Fokkink, Ortega and Rust.

public theorem_wanted kimberlingOnePosition_kimberlingZeroPosition {n : ℕ} (hn : 1 ≤ n) :
    kimberlingOnePosition (kimberlingZeroPosition n) + 1 =
        kimberlingOnePosition n + kimberlingZeroPosition n ∨
      kimberlingOnePosition (kimberlingZeroPosition n) =
        kimberlingOnePosition n + kimberlingZeroPosition n

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Theorem 3.

Uses 2

Statement usesPositions of the ones in Kimberling's word · Positions of the zeros in Kimberling's word

TheoremGutkovskiy's sequence modulo 2 is generated by a morphism#●ready to prove

Let \(g_0, g_1, g_2, \ldots\) be Gutkovskiy's sequence, and let \(u\) be the map on the alphabet \(\mathbb{N}\) with \(u(0) = 01\) and \(u(b) = 0010\) for every letter \(b \ne 0\). Then the infinite word \((g_n \bmod 2)_{n \ge 0}\) is the limit of the iterates of \(u\) at the letter \(0\). On the letters \(0\) and \(1\) that occur, \(u\) is the morphism \(0 \mapsto 01\), \(1 \mapsto 0010\), and the word is OEIS A284772.

public theorem_wanted isOmegaLimit_gutkovskiy_mod_two :
    IsOmegaLimit (fun b : ℕ ↦ if b = 0 then [0, 1] else [0, 0, 1, 0]) 0
      fun n ↦ gutkovskiy n % 2

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Theorem 4.

Uses 2

Statement usesInfinite word as the limit of iterates · Gutkovskiy's sequence

TheoremGutkovskiy's sequence from its parities#●ready to prove

Let \(g_0, g_1, \dots\) be Gutkovskiy's sequence, let \(g'_n = g_n \bmod 2\) and let \(h_n = \sum_{0 \le i < n} g'_i\). Then \(g_n = 2h_n + g'_n\) for every \(n \ge 0\).

public theorem_wanted gutkovskiy_eq_two_mul_sum_mod_two_add (n : ℕ) :
    gutkovskiy n = 2 * ∑ i ∈ Finset.range n, gutkovskiy i % 2 + gutkovskiy n % 2

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Theorem 5.

Uses 1

Statement usesGutkovskiy's sequence

TheoremLengths with two right-special factors in Kimberling's word#●ready to prove

Let \(k\) be Kimberling's word and write \(K_m\) for the length of the \(m\)-th Kimberling block. A word \(u\) is a right-special factor of \(k\) if both \(u0\) and \(u1\) are factors of \(k\). For every \(n \ge 0\), \(k\) has exactly two right-special factors of length \(n\) if and only if there is an \(i \ge 0\) such that \(x_i \le n < x_i + K_{2i}\), where \(x_i = K_1 + K_3 + \cdots + K_{2i+1}\), or \(y_i \le n < y_i + K_{2i+1}\), where \(y_i = K_0 + K_2 + \cdots + K_{2i+2}\).

public theorem_wanted rightSpecialFactors_kimberlingWord_ncard_eq_two_iff (n : ℕ) :
    (rightSpecialFactors kimberlingWord n).ncard = 2 ↔ ∃ i : ℕ,
      (∑ j ∈ Finset.range (i + 1), (kimberlingBlock (2 * j + 1)).length ≤ n ∧
        n < ∑ j ∈ Finset.range (i + 1), (kimberlingBlock (2 * j + 1)).length +
          (kimberlingBlock (2 * i)).length) ∨
      (∑ j ∈ Finset.range (i + 2), (kimberlingBlock (2 * j)).length ≤ n ∧
        n < ∑ j ∈ Finset.range (i + 2), (kimberlingBlock (2 * j)).length +
          (kimberlingBlock (2 * i + 1)).length)

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Theorem 6.

Uses 3

Statement usesKimberling's blocks · Kimberling's word · Right-special factors

TheoremFactor complexity of Kimberling's word#●ready to prove

Let \(\rho(n)\) be the factor complexity of Kimberling's word \(k\), the number of distinct factors of \(k\) of length \(n\). Then, as \(n \to \infty\) over the natural numbers, \(\limsup \rho(n)/n = (30 + \sqrt{3})/23\) and \(\liminf \rho(n)/n = (3 + \sqrt{3})/4\).

public theorem_wanted limsup_liminf_wordFactorComplexity_kimberlingWord :
    limsup (fun n : ℕ ↦ (wordFactorComplexity kimberlingWord n : ℝ) / n) atTop =
        (30 + √3) / 23 ∧
      liminf (fun n : ℕ ↦ (wordFactorComplexity kimberlingWord n : ℝ) / n) atTop =
        (3 + √3) / 4

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Corollary 1.

Uses 2

Statement usesKimberling's word · Factor complexity of an infinite word

TheoremCritical exponent of Kimberling's word#●ready to prove

Let \(k = k_1 k_2 k_3 \cdots\) be Kimberling's word. The supremum of the ratios \(m/p\), over all integers \(m \ge 1\) and \(p \ge 1\) for which some factor \(k_{i+1} k_{i+2} \cdots k_{i+m}\) of \(k\) (\(i \ge 0\)) has period \(p\), that is, \(k_{i+1+j} = k_{i+1+j+p}\) for every \(j \ge 0\) with \(j + p < m\), is \((2\sqrt{3} + 12)/3\).

Allowing every period, not only the shortest one, does not change the supremum.

public theorem_wanted sSup_exponent_kimberlingWord :
    sSup {e : ℝ | ∃ i m p : ℕ, 0 < m ∧ 0 < p ∧
      (∀ j, j + p < m → kimberlingWord (i + j) = kimberlingWord (i + j + p)) ∧
        e = m / p} = (2 * √3 + 12) / 3

Sources

• Jeffrey Shallit, Proof of Irvine's Conjecture via Mechanized Guessing, INTEGERS 24 (2024), Article A51, Theorem 7.

Uses 1

Statement usesKimberling's word

23 fully proved9 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.