Anti-recurrence and greedy subsum-free sequences

DefinitionLeast positive integer missing from a finite set#✓fully proved

For a finite set \(s\) of natural numbers, this is the least positive integer not in \(s\) (the source's \(\mathrm{mex}\) over the positive integers, used to build the anti-Tribonacci sequence). It always lies among \(1, \dots, |s| + 1\).

public def antiTribonacciMex (s : Finset ℕ) : ℕ :=
  ((List.range (s.card + 2)).find? fun m => decide (0 < m ∧ m ∉ s)).getD 0

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Used by 7

Used byThe anti-Fibonacci construction · Block of successive mex values · Mex of \(\{1, 2, 3, 6\}\) · The mex is at most every missing positive integer · The mex of a finite set lies outside the set · The mex of a finite set is positive · Anti-Tribonacci construction

TheoremMex of \(\{1, 2, 3, 6\}\)#✓fully proved

The least positive integer not in \(\{1, 2, 3, 6\}\) is \(4\).

public theorem antiTribonacciMex_example : antiTribonacciMex {1, 2, 3, 6} = 4

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 1

Statement usesLeast positive integer missing from a finite set

TheoremThe mex of a finite set is positive#✓fully proved

Write \(\mathrm{mex}(s)\) for the least positive integer not in a finite set \(s\) of natural numbers. For every such \(s\), \(\mathrm{mex}(s) > 0\).

public theorem antiTribonacciMex_pos (s : Finset ℕ) : 0 < antiTribonacciMex s

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 1

Statement usesLeast positive integer missing from a finite set

TheoremThe mex of a finite set lies outside the set#✓fully proved

Write \(\mathrm{mex}(s)\) for the least positive integer not in a finite set \(s\) of natural numbers. For every such \(s\), \(\mathrm{mex}(s) \notin s\).

public theorem antiTribonacciMex_notMem (s : Finset ℕ) : antiTribonacciMex s ∉ s

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 1

Statement usesLeast positive integer missing from a finite set

TheoremThe mex is at most every missing positive integer#✓fully proved

Write \(\mathrm{mex}(s)\) for the least positive integer not in a finite set \(s\) of natural numbers. If \(m\) is a positive integer with \(m \notin s\), then \(\mathrm{mex}(s) \le m\).

public theorem antiTribonacciMex_le_of_notMem (s : Finset ℕ) {m : ℕ} (hm : 0 < m)
    (hms : m ∉ s) : antiTribonacciMex s ≤ m

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 1

Statement usesLeast positive integer missing from a finite set

DefinitionAnti-Tribonacci construction#✓fully proved

Write \(\mathrm{mex}(U)\) for the least positive integer not in a finite set \(U\) of natural numbers. Set \((A_1, B_1, C_1, D_1) = (1, 2, 3, 6)\) and \(U_1 = \{1, 2, 3, 6\}\). For \(k \ge 1\) let \(A_{k+1} = \mathrm{mex}(U_k)\), \(B_{k+1} = \mathrm{mex}(U_k \cup \{A_{k+1}\})\), \(C_{k+1} = \mathrm{mex}(U_k \cup \{A_{k+1}, B_{k+1}\})\), \(D_{k+1} = A_{k+1} + B_{k+1} + C_{k+1}\) and \(U_{k+1} = U_k \cup \{A_{k+1}, B_{k+1}, C_{k+1}, D_{k+1}\}\). Entry \(n\) of the construction is the pair \(((A_{n+1}, B_{n+1}, C_{n+1}, D_{n+1}), U_{n+1})\), where \(U_{n+1}\) is the set of all values used so far.

public def antiTribonacciState : ℕ → (ℕ × ℕ × ℕ × ℕ) × Finset ℕ
  | 0 => ((1, 2, 3, 6), {1, 2, 3, 6})
  | n + 1 =>
    let s := (antiTribonacciState n).2
    let a := antiTribonacciMex s
    let b := antiTribonacciMex (insert a s)
    let c := antiTribonacciMex (insert b (insert a s))
    ((a, b, c, a + b + c), insert (a + b + c) (insert c (insert b (insert a s))))

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 1 · Used by 4

Statement usesLeast positive integer missing from a finite set

Used byFirst summands of the anti-Tribonacci construction · Second summands of the anti-Tribonacci construction · Third summands of the anti-Tribonacci construction · Anti-Tribonacci numbers

DefinitionFirst summands of the anti-Tribonacci construction#✓fully proved

For \(n \ge 1\), \(A_n\) is the first entry of the \(n\)-th quadruple \((A_n, B_n, C_n, D_n)\) of the anti-Tribonacci construction: \(A_1 = 1\), and for \(n \ge 2\), \(A_n\) is the least positive integer that is not among the values \(A_k\), \(B_k\), \(C_k\), \(D_k\) with \(1 \le k < n\). At \(n = 0\) the definition gives \(A_0 = A_1 = 1\).

public def antiTribonacciA (n : ℕ) : ℕ := (antiTribonacciState (n - 1)).1.1

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 1 · Used by 1

Statement usesAnti-Tribonacci construction

Used byKimberling's conjecture on the anti-Tribonacci sequence

DefinitionSecond summands of the anti-Tribonacci construction#✓fully proved

For \(n \ge 1\), \(B_n\) is the second entry of the \(n\)-th quadruple \((A_n, B_n, C_n, D_n)\) of the anti-Tribonacci construction: \(B_1 = 2\), and for \(n \ge 2\), \(B_n\) is the second smallest positive integer that is not among the values \(A_k\), \(B_k\), \(C_k\), \(D_k\) with \(1 \le k < n\). At \(n = 0\) the definition gives \(B_0 = B_1 = 2\).

public def antiTribonacciB (n : ℕ) : ℕ := (antiTribonacciState (n - 1)).1.2.1

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 1 · Used by 1

Statement usesAnti-Tribonacci construction

Used byKimberling's conjecture on the anti-Tribonacci sequence

DefinitionThird summands of the anti-Tribonacci construction#✓fully proved

For \(n \ge 1\), \(C_n\) is the third entry of the \(n\)-th quadruple \((A_n, B_n, C_n, D_n)\) of the anti-Tribonacci construction: \(C_1 = 3\), and for \(n \ge 2\), \(C_n\) is the third smallest positive integer that is not among the values \(A_k\), \(B_k\), \(C_k\), \(D_k\) with \(1 \le k < n\). At \(n = 0\) the definition gives \(C_0 = C_1 = 3\).

public def antiTribonacciC (n : ℕ) : ℕ := (antiTribonacciState (n - 1)).1.2.2.1

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 1 · Used by 1

Statement usesAnti-Tribonacci construction

Used byKimberling's conjecture on the anti-Tribonacci sequence

DefinitionAnti-Tribonacci numbers#✓fully proved

For \(n \ge 1\), the anti-Tribonacci number \(D_n\) (OEIS A265389) is the fourth entry of the \(n\)-th quadruple \((A_n, B_n, C_n, D_n)\) of the anti-Tribonacci construction, so \(D_n = A_n + B_n + C_n\) and \(D_1 = 6\). At \(n = 0\) the definition gives \(D_0 = D_1 = 6\).

public def antiTribonacciD (n : ℕ) : ℕ := (antiTribonacciState (n - 1)).1.2.2.2

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 1 · Used by 3

Statement usesAnti-Tribonacci construction

Used byFirst anti-Tribonacci anti-recurrence numbers · First anti-Tribonacci numbers · Kimberling's conjecture on the anti-Tribonacci sequence

TheoremFirst anti-Tribonacci numbers#✓fully proved

Writing \(D_n\) for the \(n\)-th anti-Tribonacci number, the first four anti-Tribonacci numbers are \(D_1 = 6\), \(D_2 = 16\), \(D_3 = 27\) and \(D_4 = 36\).

public theorem antiTribonacciD_small :
    antiTribonacciD 1 = 6 ∧ antiTribonacciD 2 = 16 ∧ antiTribonacciD 3 = 27 ∧
      antiTribonacciD 4 = 36

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 1

Statement usesAnti-Tribonacci numbers

DefinitionMembers of a greedy \(3\)-subsumfree sequence below a bound#✓fully proved

For natural numbers \(x\), \(y\) and \(z\) (the source takes \(x < y < z\)), let \(S_{x,y,z}\) consist of \(x\), \(y\), \(z\) and every natural number \(n > z\) that is not a sum \(a + b + c\) of members \(a < b < c\) of \(S_{x,y,z}\) smaller than \(n\). This definition gives, for each natural number \(m\), the finite set of members of \(S_{x,y,z}\) below \(m\).

public def greedySubsumfreeBelow (x y z : ℕ) : ℕ → Finset ℕ
  | 0 => ∅
  | m + 1 =>
    let s := greedySubsumfreeBelow x y z m
    if m = x ∨ m = y ∨ m = z ∨
        (z < m ∧ ¬ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a < b ∧ b < c ∧ a + b + c = m) then
      insert m s
    else s

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 6.

Used by 2

Used byFirst members of \(S_{1,2,3}\) · Membership in three greedy 3-subsumfree sequences

TheoremFirst members of \(S_{1,2,3}\)#✓fully proved

The members of the greedy \(3\)-subsumfree sequence \(S_{1,2,3}\) below \(26\) are exactly \(1, 2, 3, 4, 5, 13, 14, 15, 25\).

public theorem greedySubsumfreeBelow_one_two_three :
    greedySubsumfreeBelow 1 2 3 26 = {1, 2, 3, 4, 5, 13, 14, 15, 25}

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 6.

Uses 1

Statement usesMembers of a greedy \(3\)-subsumfree sequence below a bound

TheoremHajdu–Tijdeman–Varga theorem on \((x-1)^c (x+1)^d\) modulo \(3\)#●ready to prove

Let \(c\) and \(d\) be natural numbers. If none of the coefficients of \(x^0, x^1, \dots, x^{c+d}\) in the integer polynomial \((x-1)^c (x+1)^d\) is divisible by \(3\), then there are natural numbers \(i > j\) such that \(c + d + 1\) equals \(3^j\), \(2 \cdot 3^j\), \(3^i + 3^j\) or \(2 \cdot 3^i + 3^j\).

public theorem_wanted coeff_not_dvd_three_shape (c d : ℕ)
    (h : ∀ k ≤ c + d,
      ¬ (3 : ℤ) ∣ (((Polynomial.X - 1) ^ c * (Polynomial.X + 1) ^ d : Polynomial ℤ)).coeff k) :
    ∃ i j : ℕ, j < i ∧ (c + d + 1 = 3 ^ j ∨ c + d + 1 = 2 * 3 ^ j ∨
      c + d + 1 = 3 ^ i + 3 ^ j ∨ c + d + 1 = 2 * 3 ^ i + 3 ^ j)

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Theorem 10 (jis-2025-25.3.8-thm-10), citing Hajdu, Tijdeman, and Varga.

TheoremKimberling's conjecture on the anti-Tribonacci sequence#●ready to prove

Let \(A_1 = 1\), \(B_1 = 2\), \(C_1 = 3\) and \(D_1 = 6\), and for \(n \ge 1\) let \(A_{n+1} < B_{n+1} < C_{n+1}\) be the three smallest positive integers that are not among \(A_i, B_i, C_i, D_i\) for \(i \le n\), and \(D_{n+1} = A_{n+1} + B_{n+1} + C_{n+1}\) (the \(D_n\) are the anti-Tribonacci numbers). For every integer \(n \ge 1\), \(0 \le 10n - 6 - 3A_n \le 2\), \(0 \le 10n - 2 - 3B_n \le 3\), \(0 \le 10n + 1 - 3C_n \le 3\) and \(0 \le 10n - 3 - D_n \le 2\).

public theorem_wanted kimberling_antiTribonacci {n : ℕ} (hn : 1 ≤ n) :
    (0 ≤ 10 * (n : ℤ) - 6 - 3 * antiTribonacciA n ∧ 10 * (n : ℤ) - 6 - 3 * antiTribonacciA n ≤ 2) ∧
    (0 ≤ 10 * (n : ℤ) - 2 - 3 * antiTribonacciB n ∧ 10 * (n : ℤ) - 2 - 3 * antiTribonacciB n ≤ 3) ∧
    (0 ≤ 10 * (n : ℤ) + 1 - 3 * antiTribonacciC n ∧ 10 * (n : ℤ) + 1 - 3 * antiTribonacciC n ≤ 3) ∧
    (0 ≤ 10 * (n : ℤ) - 3 - antiTribonacciD n ∧ 10 * (n : ℤ) - 3 - antiTribonacciD n ≤ 2)

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Theorem 12 (jis-2025-25.3.8-thm-12).

Uses 4

Statement usesFirst summands of the anti-Tribonacci construction · Second summands of the anti-Tribonacci construction · Third summands of the anti-Tribonacci construction · Anti-Tribonacci numbers

TheoremMembership in three greedy 3-subsumfree sequences#●ready to prove

For \(x < y < z\), the greedy \(3\)-subsumfree sequence \(S_{x,y,z}\) consists of \(x\), \(y\), \(z\) and every \(m > z\) that is not the sum of three different members of \(S_{x,y,z}\) smaller than \(m\). For every positive integer \(n\): \(n \in S_{1,2,3}\) if and only if \(n \in \{1, 5, 13\}\) or \(n \bmod 23 \in \{2, 3, 4, 14, 15\}\); \(n \in S_{1,3,4}\) if and only if \(n \in \{1, 7, 19\}\) or \(n \bmod 33 \in \{3, 4, 5, 6, 20, 21, 22\}\); and \(n \in S_{1,4,5}\) if and only if \(n \in \{1, 9, 25\}\) or \(n \bmod 43 \in \{4, 5, 6, 7, 8, 26, 27, 28, 29\}\).

public theorem_wanted mem_greedySubsumfree_iff {z : ℕ} (hz : 0 < z) :
    (z ∈ greedySubsumfreeBelow 1 2 3 (z + 1) ↔
      z ∈ ({1, 5, 13} : Finset ℕ) ∨ z % 23 ∈ ({2, 3, 4, 14, 15} : Finset ℕ)) ∧
    (z ∈ greedySubsumfreeBelow 1 3 4 (z + 1) ↔
      z ∈ ({1, 7, 19} : Finset ℕ) ∨ z % 33 ∈ ({3, 4, 5, 6, 20, 21, 22} : Finset ℕ)) ∧
    (z ∈ greedySubsumfreeBelow 1 4 5 (z + 1) ↔
      z ∈ ({1, 9, 25} : Finset ℕ) ∨ z % 43 ∈ ({4, 5, 6, 7, 8, 26, 27, 28, 29} : Finset ℕ))

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Theorem 15 (jis-2025-25.3.8-thm-15).

Uses 1

Statement usesMembers of a greedy \(3\)-subsumfree sequence below a bound

DefinitionUnsums of upper Wythoff numbers#✓fully proved

A positive integer \(p\) is an upper Wythoff number when the letter at index \(p - 1\) (indices start at \(0\)) of the infinite Fibonacci word \(0100101001001\ldots\) is \(1\); that is, the upper Wythoff numbers are the positions of the letter \(1\) in the Fibonacci word counted from one. A positive integer \(x\) is an unsum (OEIS A260317) if there are no upper Wythoff numbers \(p < q\) with \(p + q = x\).

The source writes the Fibonacci word over the letters \(a\) and \(b\); its letter \(b\) is the letter \(1\) here.

public def IsUpperWythoffUnsum (x : ℕ) : Prop :=
  0 < x ∧ ¬ ∃ p < x, ∃ q < x, 0 < p ∧ p < q ∧ p + q = x ∧
    fibInf (p - 1) = true ∧ fibInf (q - 1) = true

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 2, defining unsums as the members of OEIS A260317.

Uses 1 · Used by 3

Statement usesInfinite Fibonacci word

Used byThe unsums up to 21 · Gaps between unsums · The first thirteen gaps between unsums

TheoremThe upper Wythoff numbers below 30#✓fully proved

The positive integers \(p < 30\) such that the letter at index \(p - 1\) (indices start at \(0\)) of the infinite Fibonacci word is \(1\), that is, the upper Wythoff numbers below \(30\), are exactly \(2, 5, 7, 10, 13, 15, 18, 20, 23, 26, 28\).

public theorem upperWythoff_small :
    (Finset.range 30).filter (fun p => 0 < p ∧ fibInf (p - 1) = true) =
      {2, 5, 7, 10, 13, 15, 18, 20, 23, 26, 28}

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 2.

Uses 3

Statement usesInfinite Fibonacci word

Proof usesFinite Fibonacci words agree with the infinite Fibonacci word · Finite Fibonacci words

TheoremThe unsums up to 21#✓fully proved

The unsums (OEIS A260317) that are at most \(21\) are exactly \(1, 2, 3, 4, 5, 6, 8, 10, 11, 13, 14, 16, 19, 21\).

public theorem isUpperWythoffUnsum_small :
    (Finset.range 22).filter IsUpperWythoffUnsum =
      {1, 2, 3, 4, 5, 6, 8, 10, 11, 13, 14, 16, 19, 21}

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 2.

Uses 4

Statement usesUnsums of upper Wythoff numbers

Proof usesInfinite Fibonacci word · Finite Fibonacci words agree with the infinite Fibonacci word · Finite Fibonacci words

DefinitionGaps between unsums#✓fully proved

Let \(a_1 < a_2 < \cdots\) be the unsums (OEIS A260317): the positive integers that are not a sum \(p + q\) of upper Wythoff numbers \(p < q\). For \(i \ge 0\), the \(i\)-th gap between consecutive unsums (counted from zero) is \(a_{i+2} - a_{i+1}\); this is OEIS A260311 shifted by one.

public noncomputable def upperWythoffUnsumGap (i : ℕ) : ℕ :=
  Nat.nth IsUpperWythoffUnsum (i + 1) - Nat.nth IsUpperWythoffUnsum i

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 2.

Uses 1 · Used by 6

Statement usesUnsums of upper Wythoff numbers

Used byMarkers among the unsum gaps · The last gap of size one between unsums · The first thirteen gaps between unsums · The first two markers · The first palindrome · Words between markers in the unsum gap sequence

TheoremThe first thirteen gaps between unsums#✓fully proved

Let \(a_1 < a_2 < \cdots\) be the unsums (OEIS A260317) and let \(g_i = a_{i+2} - a_{i+1}\) for \(i \ge 0\). Then the gaps \(g_0, g_1, \dots, g_{12}\) are \(1, 1, 1, 1, 1, 2, 2, 1, 2, 1, 2, 3, 2\).

public theorem upperWythoffUnsumGap_small :
    (List.range 13).map upperWythoffUnsumGap = [1, 1, 1, 1, 1, 2, 2, 1, 2, 1, 2, 3, 2]

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 2.

Uses 5 · Used by 2

Statement usesGaps between unsums

Proof usesUnsums of upper Wythoff numbers · Infinite Fibonacci word · Finite Fibonacci words agree with the infinite Fibonacci word · Finite Fibonacci words

Used byThe first two markers · The first palindrome

DefinitionMarkers among the unsum gaps#✓fully proved

A natural number \(i\) is a marker if \(i \ge 10\) and the \(i\)-th gap between consecutive unsums of upper Wythoff numbers (counted from zero) equals \(2\).

The source marks the entries \(2\) of A260311 that follow the irregular prefix \(1111122121\) of length ten.

public def IsUpperWythoffUnsumMarker (i : ℕ) : Prop :=
  10 ≤ i ∧ upperWythoffUnsumGap i = 2

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 2.

Uses 1 · Used by 2

Statement usesGaps between unsums

Used byMarkers in the gaps between unsums · The first two markers

DefinitionMarkers in the gaps between unsums#✓fully proved

Call a gap index \(i\) a marker if \(i \ge 10\) and the \(i\)-th gap between consecutive unsums (counted from zero) equals \(2\). For \(j \ge 0\), the \(j\)-th marker is the \(j\)-th marker in increasing order, counted from zero, so the \(0\)-th marker is the smallest one.

public noncomputable def upperWythoffUnsumMarker (j : ℕ) : ℕ :=
  Nat.nth IsUpperWythoffUnsumMarker j

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 2.

Uses 1 · Used by 3

Statement usesMarkers among the unsum gaps

Used byThe first two markers · The first palindrome · Words between markers in the unsum gap sequence

DefinitionWords between markers in the unsum gap sequence#✓fully proved

Let \(g_0, g_1, g_2, \ldots\) be the gaps between consecutive unsums, and call an index \(i \ge 10\) with \(g_i = 2\) a marker. Let \(m_0 < m_1 < m_2 < \cdots\) be the markers in increasing order. For each \(j\), the \(j\)-th word between markers is \(g_{m_j + 1} g_{m_j + 2} \cdots g_{m_{j+1} - 1}\), the word of the gaps strictly between the \(j\)-th and the \((j+1)\)-th marker.

The source writes the gap sequence after its prefix as \(2 W_1 2 W_1 2 W_2 2 W_2 2 W_3 2 \cdots\), so these words are \(W_1, W_1, W_2, W_2, \ldots\).

public noncomputable def upperWythoffUnsumWord (j : ℕ) : List ℕ :=
  (List.range' (upperWythoffUnsumMarker j + 1)
    (upperWythoffUnsumMarker (j + 1) - upperWythoffUnsumMarker j - 1)).map upperWythoffUnsumGap

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 2.

Uses 2 · Used by 4

Statement usesGaps between unsums · Markers in the gaps between unsums

Used byThe words \(W_i\) of the unsum gap sequence · A word \(3V3\) between markers is followed by a word starting with \(3V\) · Digit sums of the words between markers · Digit sums between markers are two less than Fibonacci numbers

DefinitionThe words \(W_i\) of the unsum gap sequence#✓fully proved

For \(i \ge 1\), the word \(W_i\) is the word of gaps strictly between the \((2i-2)\)-th and \((2i-1)\)-th markers of the unsum gap sequence, with markers counted from zero; for \(i = 0\) the definition gives the same word as for \(i = 1\).

public noncomputable def upperWythoffUnsumPalindrome (i : ℕ) : List ℕ :=
  upperWythoffUnsumWord (2 * i - 2)

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 2.

Uses 1 · Used by 6

Statement usesWords between markers in the unsum gap sequence

Used byThe palindromes begin and end with the digit 3 · When one palindrome is a prefix of the next · The first palindrome · The gap words are palindromes · Recursion for the words \(W_i\) of the unsum gap sequence · The words \(W_i\) converge to \(3\) followed by the coded Fibonacci word

TheoremThe first two markers#✓fully proved

Call a gap index \(i\) a marker if \(i \ge 10\) and the \(i\)-th gap between consecutive unsums (counted from zero) equals \(2\). The smallest marker is \(10\) and the second smallest is \(12\).

public theorem upperWythoffUnsumMarker_zero_one :
    upperWythoffUnsumMarker 0 = 10 ∧ upperWythoffUnsumMarker 1 = 12

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 2.

Uses 4 · Used by 1

Statement usesMarkers in the gaps between unsums

Proof usesMarkers among the unsum gaps · Gaps between unsums · The first thirteen gaps between unsums

Used byThe first palindrome

TheoremThe first palindrome#✓fully proved

Let \(g_k\) be the \(k\)-th gap between consecutive unsums (OEIS A260317), counted from zero, and let \(m_0 < m_1 < \cdots\) be the markers, the indices \(k \ge 10\) with \(g_k = 2\), in increasing order. The word \(W_1\) of the gaps \(g_k\) with \(m_0 < k < m_1\), in increasing order of \(k\), consists of the single digit \(3\).

public theorem upperWythoffUnsumPalindrome_one : upperWythoffUnsumPalindrome 1 = [3]

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 2.

Uses 5

Statement usesThe words \(W_i\) of the unsum gap sequence

Proof usesGaps between unsums · The first thirteen gaps between unsums · Markers in the gaps between unsums · The first two markers

TheoremThe last gap of size one between unsums#●ready to prove

Let \(a_1 < a_2 < \cdots\) be the unsums (OEIS A260317), and for \(i \ge 0\) let \(g_i = a_{i+2} - a_{i+1}\) be the \(i\)-th gap between consecutive unsums, counted from zero. Then \(g_9 = 1\), and \(g_i \ne 1\) for every \(i \ge 10\).

public theorem_wanted upperWythoffUnsumGap_ne_one :
    upperWythoffUnsumGap 9 = 1 ∧ ∀ i, 10 ≤ i → upperWythoffUnsumGap i ≠ 1

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Lemma 1 (jis-2025-25.3.8-lem-1).

Uses 1

Statement usesGaps between unsums

TheoremDigit sums between markers are two less than Fibonacci numbers#●ready to prove

For every \(j\), the digit sum of the \(j\)-th word between markers of the unsum gap sequence, plus \(2\), is a Fibonacci number: it equals \(F_m\) for some natural number \(m\).

public theorem_wanted upperWythoffUnsumWord_sum_add_two_isFib (j : ℕ) :
    ∃ m, (upperWythoffUnsumWord j).sum + 2 = Nat.fib m

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Lemma 2 (jis-2025-25.3.8-lem-2).

Uses 1

Statement usesWords between markers in the unsum gap sequence

TheoremDigit sums of the words between markers#●ready to prove

Let \(F_n\) be the Fibonacci numbers, with \(F_0 = 0\) and \(F_1 = 1\). For every \(j\) (words counted from zero), the digit sum of the \(j\)-th word between markers of the unsum gap sequence, plus \(2\), equals \(F_{\lfloor j/2 \rfloor + 5}\).

So the digit sums are \(3, 3, 6, 6, 11, \ldots\); adding the preceding marker digit \(2\) gives \(F_5, F_5, F_6, F_6, F_7, \ldots\), which is how the source's Lemma 3 must be read, since the bare digit sum of the first word is \(3 \ne F_5 = 5\).

public theorem_wanted upperWythoffUnsumWord_sum_add_two (j : ℕ) :
    (upperWythoffUnsumWord j).sum + 2 = Nat.fib (j / 2 + 5)

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Lemma 3 (jis-2025-25.3.8-lem-3).

Uses 1

Statement usesWords between markers in the unsum gap sequence

TheoremThe gap words are palindromes#●ready to prove

Let \(g_k\) be the \(k\)-th gap between consecutive unsums (OEIS A260317), counted from zero, and let \(m_0 < m_1 < \cdots\) be the markers, the indices \(k \ge 10\) with \(g_k = 2\), in increasing order. For \(i \ge 1\) let \(W_i\) be the word of the gaps \(g_k\) with \(m_{2i-2} < k < m_{2i-1}\), in increasing order of \(k\). Then for every \(i \ge 1\), the word \(W_i\) read backwards is \(W_i\) itself.

public theorem_wanted upperWythoffUnsumPalindrome_reverse {i : ℕ} (hi : 1 ≤ i) :
    (upperWythoffUnsumPalindrome i).reverse = upperWythoffUnsumPalindrome i

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Lemma 4 (jis-2025-25.3.8-lem-4).

Uses 1

Statement usesThe words \(W_i\) of the unsum gap sequence

TheoremThe palindromes begin and end with the digit 3#●ready to prove

Let \(g_k\) be the \(k\)-th gap between consecutive unsums (OEIS A260317), counted from zero, and let \(m_0 < m_1 < \cdots\) be the markers, the indices \(k \ge 10\) with \(g_k = 2\), in increasing order. For \(i \ge 1\) let \(W_i\) be the word of the gaps \(g_k\) with \(m_{2i-2} < k < m_{2i-1}\), in increasing order of \(k\). Then for every \(i \ge 1\), the word \(W_i\) is nonempty, its first digit is \(3\), and its last digit is \(3\).

public theorem_wanted upperWythoffUnsumPalindrome_head_getLast {i : ℕ} (hi : 1 ≤ i) :
    (upperWythoffUnsumPalindrome i).head? = some 3 ∧
      (upperWythoffUnsumPalindrome i).getLast? = some 3

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Lemma 5 (jis-2025-25.3.8-lem-5).

Uses 1

Statement usesThe words \(W_i\) of the unsum gap sequence

TheoremA word \(3V3\) between markers is followed by a word starting with \(3V\)#●ready to prove

Let \(V\) be a finite word of natural numbers, and suppose that the \(j\)-th word between markers of the unsum gap sequence is \(3V3\). Then \(3V\) is a prefix of the \((j+1)\)-th word between markers, and if the \((j+1)\)-th word has the same digit sum as the \(j\)-th word, then the two words are equal.

public theorem_wanted upperWythoffUnsumWord_prefix_next {j : ℕ} {V : List ℕ}
    (h : upperWythoffUnsumWord j = 3 :: V ++ [3]) :
    (3 :: V) <+: upperWythoffUnsumWord (j + 1) ∧
      ((upperWythoffUnsumWord (j + 1)).sum = (upperWythoffUnsumWord j).sum →
        upperWythoffUnsumWord (j + 1) = upperWythoffUnsumWord j)

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Lemma 6 (jis-2025-25.3.8-lem-6).

Uses 1

Statement usesWords between markers in the unsum gap sequence

TheoremWhen one palindrome is a prefix of the next#●ready to prove

Let \(g_k\) be the \(k\)-th gap between consecutive unsums (OEIS A260317), counted from zero, and let \(m_0 < m_1 < \cdots\) be the markers, the indices \(k \ge 10\) with \(g_k = 2\), in increasing order. For \(i \ge 1\) let \(W_i\) be the word of the gaps \(g_k\) with \(m_{2i-2} < k < m_{2i-1}\), in increasing order of \(k\). Then for every \(i \ge 1\), the word \(W_i\) is a prefix of \(W_{i+1}\) if and only if \(i\) is odd.

public theorem_wanted upperWythoffUnsumPalindrome_isPrefix_succ_iff {i : ℕ} (hi : 1 ≤ i) :
    upperWythoffUnsumPalindrome i <+: upperWythoffUnsumPalindrome (i + 1) ↔ Odd i

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Lemma 7 (jis-2025-25.3.8-lem-7).

Uses 1

Statement usesThe words \(W_i\) of the unsum gap sequence

TheoremRecursion for the words \(W_i\) of the unsum gap sequence#●ready to prove

For each \(i\) let \(V_i\) be the word \(W_i\) with its first and last digit removed, write \(|W|\) for the length of a word \(W\), and denote concatenation of words by juxtaposition. For every \(i \ge 2\): if \(i\) is odd, then \(W_{i+1} = W_i \, 5 \, V_{i-1} \, 3\); if \(i\) is even, then \(W_{i+1} = 3 \, V_i \, 5 \, W_{i-1}\); and in both cases \(|W_{i+1}| = |W_i| + |W_{i-1}|\). Moreover \(|W_1| = 1\), \(|W_2| = 2\), and \(|W_i| = F_{i+1}\) for every \(i \ge 1\), where \(F_m\) is the \(m\)-th Fibonacci number (\(F_0 = 0\), \(F_1 = 1\)).

public theorem_wanted upperWythoffUnsumPalindrome_succ :
    (∀ i, 2 ≤ i →
      (Odd i → upperWythoffUnsumPalindrome (i + 1) = upperWythoffUnsumPalindrome i ++
        5 :: (upperWythoffUnsumPalindrome (i - 1)).tail.dropLast ++ [3]) ∧
      (Even i → upperWythoffUnsumPalindrome (i + 1) =
        3 :: (upperWythoffUnsumPalindrome i).tail.dropLast ++
          5 :: upperWythoffUnsumPalindrome (i - 1)) ∧
      (upperWythoffUnsumPalindrome (i + 1)).length =
        (upperWythoffUnsumPalindrome i).length + (upperWythoffUnsumPalindrome (i - 1)).length) ∧
    (upperWythoffUnsumPalindrome 1).length = 1 ∧ (upperWythoffUnsumPalindrome 2).length = 2 ∧
    ∀ i, 1 ≤ i → (upperWythoffUnsumPalindrome i).length = Nat.fib (i + 1)

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Lemma 8 (jis-2025-25.3.8-lem-8).

Uses 1

Statement usesThe words \(W_i\) of the unsum gap sequence

TheoremThe words \(W_i\) converge to \(3\) followed by the coded Fibonacci word#●ready to prove

Let \(u_0 u_1 u_2 \cdots\) be the infinite Fibonacci word over \(\{0, 1\}\), indexed from \(0\), and let \(\mathbf{V}\) be the infinite word obtained from it by replacing each \(0\) by \(5\) and each \(1\) by \(3\). Then the words \(W_i\) of the unsum gap sequence converge to the infinite word \(3\mathbf{V}\): for every \(k \ge 0\) there is \(N\) such that for every \(i \ge N\) the word \(W_i\) has more than \(k\) digits and its digit at position \(k\) (counted from zero) is the digit of \(3\mathbf{V}\) at position \(k\), that is, \(3\) if \(k = 0\), and for \(k \ge 1\) it is \(3\) if \(u_{k-1} = 1\) and \(5\) if \(u_{k-1} = 0\).

public theorem_wanted upperWythoffUnsumPalindrome_tendsto (k : ℕ) :
    ∃ N, ∀ i, N ≤ i → (upperWythoffUnsumPalindrome i)[k]? =
      some (if k = 0 then 3 else if fibInf (k - 1) = true then 3 else 5)

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Lemma 9 (jis-2025-25.3.8-lem-9).

Uses 2

Statement usesInfinite Fibonacci word · The words \(W_i\) of the unsum gap sequence

DefinitionIterates of the period-doubling substitution#✓fully proved

Write the period-doubling substitution \(a \mapsto ab\), \(b \mapsto aa\) over the letters \(a = 1\) and \(b = 0\), so that it sends \(1\) to \(10\) and \(0\) to \(11\). The \(n\)-th period-doubling iterate is the word obtained by applying this substitution \(n\) times to the one-letter word \(1\); the iterates begin \(1\), \(10\), \(1011\), \(10111010\), and their limit is the period-doubling word (Walnut's PD).

The source's prose takes \(a = 0\) and \(b = 1\), but its Walnut definition antifib (PD[k]=@1 gives \(9 + 10k\)) and its displayed anti-Fibonacci numbers \(0, 3, 9, 13, \ldots\) need the first letter of PD to be \(1\).

public def periodDoublingWord : ℕ → List ℕ
  | 0 => [1]
  | n + 1 => (periodDoublingWord n).flatMap fun c => if c = 1 then [1, 0] else [1, 1]

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Used by 3

Used byLength of the period-doubling iterates · The period-doubling word · Letters of the period-doubling iterates

DefinitionThe period-doubling word#✓fully proved

For a natural number \(k\), the letter at index \(k\) (indices start at \(0\)) of the period-doubling word is the letter at index \(k\) of the word obtained by applying the period-doubling substitution \(1 \mapsto 10\), \(0 \mapsto 11\) to the one-letter word \(1\) a total of \(\lfloor \log_2 k \rfloor + 1\) times, where \(\lfloor \log_2 0 \rfloor\) is taken to be \(0\). That word has length \(2^{\lfloor \log_2 k \rfloor + 1} \le 2k + 2\), so it contains index \(k\).

public def periodDoubling (k : ℕ) : ℕ := (periodDoublingWord (Nat.log 2 k + 1)).getD k 0

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 1 · Used by 3

Statement usesIterates of the period-doubling substitution

Used byFirst letters of the period-doubling word · Letters of the period-doubling iterates · Zaslavsky's formulas for the anti-Fibonacci numbers

TheoremLength of the period-doubling iterates#✓fully proved

For every natural number \(n\), the word obtained by applying the period-doubling substitution \(1 \mapsto 10\), \(0 \mapsto 11\) to the one-letter word \(1\) a total of \(n\) times has length \(2^n\).

public theorem length_periodDoublingWord (n : ℕ) : (periodDoublingWord n).length = 2 ^ n

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 1 · Used by 1

Statement usesIterates of the period-doubling substitution

Used byLetters of the period-doubling iterates

TheoremLetters of the period-doubling iterates#✓fully proved

Let \(w_m\) be the word obtained by applying the period-doubling substitution \(1 \mapsto 10\), \(0 \mapsto 11\) to the one-letter word \(1\) a total of \(m\) times. For all natural numbers \(m\) and \(k\) with \(k < 2^m\), the letter of \(w_m\) at index \(k\) (indices start at \(0\)) equals the letter of the period-doubling word at index \(k\).

public theorem periodDoublingWord_getD {m k : ℕ} (hk : k < 2 ^ m) :
    (periodDoublingWord m).getD k 0 = periodDoubling k

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 3

Statement usesThe period-doubling word · Iterates of the period-doubling substitution

Proof usesLength of the period-doubling iterates

TheoremFirst letters of the period-doubling word#✓fully proved

The letters at indices \(0, 1, \ldots, 7\) of the period-doubling word (the fixed point of \(1 \mapsto 10\), \(0 \mapsto 11\) that starts with \(1\)) are \(1, 0, 1, 1, 1, 0, 1, 0\).

public theorem periodDoubling_small :
    (List.range 8).map periodDoubling = [1, 0, 1, 1, 1, 0, 1, 0]

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 1

Statement usesThe period-doubling word

DefinitionThe anti-Fibonacci construction#✓fully proved

For each \(n \ge 0\), entry \(n\) of the construction is the triple \((A_{n+1}, B_{n+1}, C_{n+1})\) of natural numbers together with the finite set \(U_{n+1}\) of values used so far. Entry \(0\) is \((1, 2, 3)\) with \(U_1 = \{1, 2, 3\}\). For \(n \ge 1\), \(A_{n+1}\) is the least positive integer not in \(U_n\), \(B_{n+1}\) is the least positive integer not in \(U_n \cup \{A_{n+1}\}\), \(C_{n+1} = A_{n+1} + B_{n+1}\), and \(U_{n+1} = U_n \cup \{A_{n+1}, B_{n+1}, C_{n+1}\}\).

The \(C_n\) are the anti-Fibonacci numbers (OEIS A075326 without its initial \(0\)) and the missing numbers \(A_1, B_1, A_2, B_2, \dots\) are the non-anti-Fibonacci numbers \(Y_1, Y_2, \dots\) (OEIS A249031).

public def antiFibonacciState : ℕ → (ℕ × ℕ × ℕ) × Finset ℕ
  | 0 => ((1, 2, 3), {1, 2, 3})
  | n + 1 =>
    let s := (antiFibonacciState n).2
    let a := antiTribonacciMex s
    let b := antiTribonacciMex (insert a s)
    ((a, b, a + b), insert (a + b) (insert b (insert a s)))

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 1 · Used by 3

Statement usesLeast positive integer missing from a finite set

Used byFirst summands of the anti-Fibonacci construction · Second summands of the anti-Fibonacci construction · Anti-Fibonacci numbers

DefinitionFirst summands of the anti-Fibonacci construction#✓fully proved

For \(n \ge 1\), \(A_n\) is the first entry of the \(n\)-th triple \((A_n, B_n, C_n)\) of the anti-Fibonacci construction: \(A_1 = 1\), and for \(n \ge 2\), \(A_n\) is the least positive integer that is not among the values \(A_k\), \(B_k\), \(C_k\) with \(1 \le k < n\). At \(n = 0\) the definition gives \(A_0 = A_1 = 1\).

In the source's notation \(A_n = Y_{2n-1}\), where \(Y_1 < Y_2 < \dots\) are the non-anti-Fibonacci numbers.

public def antiFibonacciA (n : ℕ) : ℕ := (antiFibonacciState (n - 1)).1.1

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 1 · Used by 2

Statement usesThe anti-Fibonacci construction

Used byFirst anti-Fibonacci and non-anti-Fibonacci numbers · Zaslavsky's formulas for the anti-Fibonacci numbers

DefinitionSecond summands of the anti-Fibonacci construction#✓fully proved

For \(n \ge 1\), \(B_n\) is the second entry of the \(n\)-th triple \((A_n, B_n, C_n)\) of the anti-Fibonacci construction: \(B_1 = 2\), and for \(n \ge 2\), \(B_n\) is the second smallest positive integer that is not among the values \(A_k\), \(B_k\), \(C_k\) with \(1 \le k < n\). At \(n = 0\) the definition gives \(B_0 = B_1 = 2\).

In the source's notation \(B_n = Y_{2n}\), where \(Y_1 < Y_2 < \dots\) are the non-anti-Fibonacci numbers.

public def antiFibonacciB (n : ℕ) : ℕ := (antiFibonacciState (n - 1)).1.2.1

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 1 · Used by 2

Statement usesThe anti-Fibonacci construction

Used byFirst anti-Fibonacci and non-anti-Fibonacci numbers · Zaslavsky's formulas for the anti-Fibonacci numbers

DefinitionAnti-Fibonacci numbers#✓fully proved

For \(n \ge 1\), the anti-Fibonacci number \(X_n = C_n\) is the third entry of the \(n\)-th triple \((A_n, B_n, C_n)\) of the anti-Fibonacci construction, so \(C_n = A_n + B_n\) and \(C_1 = 3\). At \(n = 0\) the definition gives \(C_0 = C_1 = 3\).

public def antiFibonacciC (n : ℕ) : ℕ := (antiFibonacciState (n - 1)).1.2.2

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 1 · Used by 3

Statement usesThe anti-Fibonacci construction

Used byFirst anti-Fibonacci and non-anti-Fibonacci numbers · First anti-Fibonacci anti-recurrence numbers · Zaslavsky's formulas for the anti-Fibonacci numbers

TheoremFirst anti-Fibonacci and non-anti-Fibonacci numbers#✓fully proved

In the anti-Fibonacci construction with triples \((A_n, B_n, C_n)\), the first four anti-Fibonacci numbers are \(C_1 = 3\), \(C_2 = 9\), \(C_3 = 13\) and \(C_4 = 18\), and \((A_1, B_1) = (1, 2)\), \((A_2, B_2) = (4, 5)\), \((A_3, B_3) = (6, 7)\) and \((A_4, B_4) = (8, 10)\).

Since \(A_1, B_1, A_2, B_2, \dots\) are the non-anti-Fibonacci numbers, the first eight non-anti-Fibonacci numbers are \(1, 2, 4, 5, 6, 7, 8, 10\).

public theorem antiFibonacci_small :
    (List.range 4).map (fun n => antiFibonacciC (n + 1)) = [3, 9, 13, 18] ∧
      (List.range 4).map (fun n => (antiFibonacciA (n + 1), antiFibonacciB (n + 1))) =
        [(1, 2), (4, 5), (6, 7), (8, 10)]

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Section 4.

Uses 3

Statement usesFirst summands of the anti-Fibonacci construction · Second summands of the anti-Fibonacci construction · Anti-Fibonacci numbers

TheoremZaslavsky's formulas for the anti-Fibonacci numbers#●ready to prove

Let \(A_1 = 1\), \(B_1 = 2\), \(C_1 = 3\), and for \(n \ge 1\) let \(A_{n+1} < B_{n+1}\) be the two smallest positive integers not among \(A_1, B_1, C_1, \ldots, A_n, B_n, C_n\) and \(C_{n+1} = A_{n+1} + B_{n+1}\). Let \(\mathrm{PD}[0], \mathrm{PD}[1], \ldots\) be the letters of the period-doubling word, the fixed point of \(1 \mapsto 10\), \(0 \mapsto 11\) starting with \(1\). Then for every \(k \ge 0\), \(C_{2k+1} = 10k + 3\), \(C_{2k+2} = 10k + 8 + \mathrm{PD}[k]\), \(A_{2k+1} = 5k + 1\), \(B_{2k+1} = 5k + 2\), \(A_{2k+2} = 5k + 3 + \mathrm{PD}[k]\), and \(B_{2k+2} = 5(k + 1)\).

In the source's notation the anti-Fibonacci numbers are \(X_n = C_n\) and the non-anti-Fibonacci numbers are \(Y_{2n-1} = A_n\) and \(Y_{2n} = B_n\), so the formulas read \(X_{2k+1} = 10k + 3\), \(X_{2k+2} = 10k + 8 + \mathrm{PD}[k]\), \(Y_{4k+1} = 5k + 1\), \(Y_{4k+2} = 5k + 2\), \(Y_{4k+3} = 5k + 3 + \mathrm{PD}[k]\) and \(Y_{4k+4} = 5(k + 1)\) (the source's \(Y_{4k} = 5k\) for \(k \ge 1\)). The source's prose writes the period-doubling word over letters \(a, b\) with \(a = 0\), but its Walnut code and its values \(X_2 = 9\) and \(Y_3 = 4\) need \(\mathrm{PD}[0] = 1\).

public theorem_wanted zaslavsky_antiFibonacci (k : ℕ) :
    antiFibonacciC (2 * k + 1) = 3 + 10 * k ∧
      antiFibonacciC (2 * k + 2) = 8 + 10 * k + periodDoubling k ∧
      antiFibonacciA (2 * k + 1) = 5 * k + 1 ∧ antiFibonacciB (2 * k + 1) = 5 * k + 2 ∧
      antiFibonacciA (2 * k + 2) = 5 * k + 3 + periodDoubling k ∧
      antiFibonacciB (2 * k + 2) = 5 * (k + 1)

Sources

• Bosma, Bruin, Fokkink, Grube, Reuijl, and Tromp, Using Walnut to Solve Problems from the OEIS, Journal of Integer Sequences 28 (2025), Article 25.3.8, Theorem 11 (jis-2025-25.3.8-thm-11), due to Zaslavsky.

Uses 4

Statement usesFirst summands of the anti-Fibonacci construction · Second summands of the anti-Fibonacci construction · Anti-Fibonacci numbers · The period-doubling word

DefinitionBlock of successive mex values#✓fully proved

For a natural number \(m\) and a finite set \(s\) of natural numbers, the mex block of length \(m\) from \(s\) is the list \((x_1, \dots, x_m)\) in which each \(x_j\) is the least positive integer not in \(s \cup \{x_1, \dots, x_{j-1}\}\).

def antiRecurrenceBlock : ℕ → Finset ℕ → List ℕ
  | 0, _ => []
  | m + 1, s => antiTribonacciMex s :: antiRecurrenceBlock m (insert (antiTribonacciMex s) s)

Sources

• Robbert Fokkink and Gandhar Joshi, Anti-Recurrence Sequences, INTEGERS 26 (2026), Article A24, Section 2 (proof of Lemma 2, the mex rule).

Uses 1 · Used by 1

Statement usesLeast positive integer missing from a finite set

Used byState of the anti-recurrence construction

DefinitionState of the anti-recurrence construction#✓fully proved

Let \(a = (a_1, \dots, a_k)\) be a finite list of natural numbers. The state at step \(0\) is the pair of the empty list and the empty set. If the state at step \(n\) has set \(S\), then the state at step \(n + 1\) is the pair \((\beta, S')\), where \(\beta = (x_1, \dots, x_k)\) is the mex block of length \(k\) from \(S\) (each \(x_j\) is the least positive integer not in \(S \cup \{x_1, \dots, x_{j-1}\}\)) and \(S' = S \cup \{x_1, \dots, x_k\} \cup \{a_1 x_1 + \dots + a_k x_k\}\).

In the notation of the source, for \(n \ge 1\) the block at step \(n\) is \((B_{(n-1)k+1}, \dots, B_{nk})\) and the set at step \(n\) is \(\{B_1, \dots, B_{nk}\} \cup \{A_1, \dots, A_n\}\), where the \(B_m\) are the non-anti-recurrence numbers and the \(A_m\) are the anti-recurrence numbers of \(a\).

def antiRecurrenceState (a : List ℕ) : ℕ → List ℕ × Finset ℕ
  | 0 => ([], ∅)
  | n + 1 =>
    let s := (antiRecurrenceState a n).2
    let blk := antiRecurrenceBlock a.length s
    (blk, insert (List.zipWith (· * ·) a blk).sum (s ∪ blk.toFinset))

Sources

• Robbert Fokkink and Gandhar Joshi, Anti-Recurrence Sequences, INTEGERS 26 (2026), Article A24, Section 2 (definition of anti-recurrence sequences and Lemma 2).

Uses 1 · Used by 2

Statement usesBlock of successive mex values

Used byAnti-recurrence numbers · Non-anti-recurrence numbers

DefinitionAnti-recurrence numbers#✓fully proved

Let \(a = (a_1, \dots, a_k)\) be a linear form with natural number coefficients. The non-anti-recurrence numbers \(B_1, B_2, \dots\) are produced in blocks of \(k\) by the mex rule, and each block \(B_{(n-1)k+1}, \dots, B_{nk}\) generates the anti-recurrence number \(A_n = \sum_{j=1}^{k} a_j B_{(n-1)k+j}\). Here \(B_m\) is the least positive integer that differs from \(B_1, \dots, B_{m-1}\) and from the anti-recurrence numbers of earlier blocks. By convention \(A_0 = 0\), following Hofstadter.

def antiRecurrence (a : List ℕ) (n : ℕ) : ℕ :=
  (List.zipWith (· * ·) a (antiRecurrenceState a n).1).sum

Sources

• Robbert Fokkink and Gandhar Joshi, Anti-Recurrence Sequences, INTEGERS 26 (2026), Article A24, Section 2 (definition of anti-recurrence sequences).

Uses 1 · Used by 12

Statement usesState of the anti-recurrence construction

Used byIntervals and residues of the anti-\(k\)-bonacci numbers · Kimberling's bounds for the anti-Jacobsthal numbers · Kimberling's bounds for the anti-Pell numbers · Gaps between successive anti-recurrence numbers · First anti-Fibonacci anti-recurrence numbers · First anti-Jacobsthal numbers · First anti-Pell numbers · First anti-Tribonacci anti-recurrence numbers · Interval location of anti-recurrence numbers for bounded forms · Lower bound for the first anti-recurrence number · Bounded anti-recurrence sequences are automatic up to a linear term · Characterization of anti-recurrence sequences

DefinitionNon-anti-recurrence numbers#✓fully proved

Let \(a = (a_1, \dots, a_k)\) be a linear form with natural number coefficients. Its non-anti-recurrence numbers \(B_1, B_2, \dots\) are produced in blocks of \(k\) by the mex rule: for \(n \ge 1\), each of \(B_{(n-1)k+1}, \dots, B_{nk}\) in turn is the least positive integer not among \(B_1, \dots, B_{(n-1)k}\), the anti-recurrence numbers \(A_1, \dots, A_{n-1}\) and the earlier entries of its block, and then \(A_n = a_1 B_{(n-1)k+1} + \dots + a_k B_{nk}\). For \(k = 2\) the subsequences \(B^1_n = B_{2n-1}\) and \(B^2_n = B_{2n}\) are the paper's \(B^1\) and \(B^2\).

By Lemma 2 of the source, for a positive form with \(k > 1\) the numbers \(B_m\) are the positive integers that are not anti-recurrence numbers, listed in increasing order.

def antiRecurrenceComplement (a : List ℕ) (m : ℕ) : ℕ :=
  (antiRecurrenceState a ((m - 1) / a.length + 1)).1.getD ((m - 1) % a.length) 0

Sources

• Robbert Fokkink and Gandhar Joshi, Anti-Recurrence Sequences, INTEGERS 26 (2026), Article A24, Section 2 (definition of anti-recurrence sequences).

Uses 1 · Used by 6

Statement usesState of the anti-recurrence construction

Used byKimberling's bounds for the anti-Jacobsthal numbers · Kimberling's bounds for the anti-Pell numbers · Gaps between successive anti-recurrence numbers · First anti-Pell numbers · Interval location of anti-recurrence numbers for bounded forms · Characterization of anti-recurrence sequences

TheoremFirst anti-Fibonacci anti-recurrence numbers#✓fully proved

The anti-recurrence numbers \(A_1, A_2, A_3, A_4\) of the linear form \((1, 1)\) are \(3, 9, 13, 18\), and the first four anti-Fibonacci numbers \(C_1, C_2, C_3, C_4\) of the Walnut anti-Fibonacci construction (OEIS A075326) are also \(3, 9, 13, 18\); so the two sequences agree for \(1 \le n \le 4\).

theorem antiRecurrence_antiFibonacci_small :
    (List.range 4).map (fun n => antiRecurrence [1, 1] (n + 1)) = [3, 9, 13, 18] ∧
      (List.range 4).map (fun n => antiFibonacciC (n + 1)) = [3, 9, 13, 18]

Sources

• Robbert Fokkink and Gandhar Joshi, Anti-Recurrence Sequences, INTEGERS 26 (2026), Article A24, Section 1.

Uses 2

Statement usesAnti-Fibonacci numbers · Anti-recurrence numbers

TheoremFirst anti-Pell numbers#✓fully proved

The anti-recurrence numbers \(A_1, A_2, A_3, A_4\) of the linear form \((1, 2)\), the anti-Pell numbers (OEIS A304502), are \(5, 11, 20, 26\), and its first eight non-anti-recurrence numbers \(B_1, \dots, B_8\) are \(1, 2, 3, 4, 6, 7, 8, 9\) (so \(B^1_n = B_{2n-1}\) starts \(1, 3, 6, 8\) and \(B^2_n = B_{2n}\) starts \(2, 4, 7, 9\)).

theorem antiRecurrence_antiPell_small :
    (List.range 4).map (fun n => antiRecurrence [1, 2] (n + 1)) = [5, 11, 20, 26] ∧
      (List.range 8).map (fun m => antiRecurrenceComplement [1, 2] (m + 1)) =
        [1, 2, 3, 4, 6, 7, 8, 9]

Sources

• Robbert Fokkink and Gandhar Joshi, Anti-Recurrence Sequences, INTEGERS 26 (2026), Article A24, Section 3.

Uses 2

Statement usesAnti-recurrence numbers · Non-anti-recurrence numbers

TheoremFirst anti-Jacobsthal numbers#✓fully proved

The anti-recurrence numbers \(A_1, A_2, A_3, A_4\) of the linear form \((2, 1)\), the anti-Jacobsthal numbers (OEIS A304499), are \(4, 11, 19, 25\).

theorem antiRecurrence_antiJacobsthal_small :
    (List.range 4).map (fun n => antiRecurrence [2, 1] (n + 1)) = [4, 11, 19, 25]

Sources

• Robbert Fokkink and Gandhar Joshi, Anti-Recurrence Sequences, INTEGERS 26 (2026), Article A24, Section 3.

Uses 1

Statement usesAnti-recurrence numbers

TheoremFirst anti-Tribonacci anti-recurrence numbers#✓fully proved

The anti-recurrence numbers \(A_1, A_2, A_3, A_4\) of the linear form \((1, 1, 1)\) are \(6, 16, 27, 36\), and the first four anti-Tribonacci numbers \(D_1, D_2, D_3, D_4\) of the Walnut anti-Tribonacci construction (OEIS A265389) are also \(6, 16, 27, 36\); so the two sequences agree for \(1 \le n \le 4\).

theorem antiRecurrence_antiTribonacci_small :
    (List.range 4).map (fun n => antiRecurrence [1, 1, 1] (n + 1)) = [6, 16, 27, 36] ∧
      (List.range 4).map (fun n => antiTribonacciD (n + 1)) = [6, 16, 27, 36]

Sources

• Robbert Fokkink and Gandhar Joshi, Anti-Recurrence Sequences, INTEGERS 26 (2026), Article A24, Section 4.

Uses 2

Statement usesAnti-recurrence numbers · Anti-Tribonacci numbers

TheoremGaps between successive anti-recurrence numbers#●ready to prove

Let \(a = (a_1, \dots, a_k)\) be a linear form with positive integer coefficients and \(k > 1\), let \(\tau = a_1 + \dots + a_k\) be its trace, and let \(A_n\) and \(B_m\) be the anti-recurrence and non-anti-recurrence numbers of \(a\); for \(m \ge 1\), block \(m\) consists of \(B_{(m-1)k+1}, \dots, B_{mk}\), and it is an interval when \(B_{mk} = B_{(m-1)k+1} + k - 1\). Then for every \(n \ge 1\) we have \(A_{n+1} \ge A_n + k\tau\). Equality holds if \(B_{(n-1)k+1+j} = B_{(n-1)k+1} + j\) for every \(j\) with \(0 \le j < 2k\), that is, if \(B_{(n-1)k+1}, \dots, B_{(n+1)k}\) are consecutive integers. The inequality is strict if exactly one of the blocks \(n\) and \(n + 1\) is an interval.

public theorem_wanted antiRecurrence_add_length_mul_sum_le (a : List ℕ) (ha : ∀ x ∈ a, 0 < x)
    (hk : 1 < a.length) {n : ℕ} (hn : 1 ≤ n) :
    antiRecurrence a n + a.length * a.sum ≤ antiRecurrence a (n + 1) ∧
      ((∀ j < 2 * a.length, antiRecurrenceComplement a ((n - 1) * a.length + j + 1) =
          antiRecurrenceComplement a ((n - 1) * a.length + 1) + j) →
        antiRecurrence a (n + 1) = antiRecurrence a n + a.length * a.sum) ∧
      (¬ (antiRecurrenceComplement a (n * a.length) =
            antiRecurrenceComplement a ((n - 1) * a.length + 1) + (a.length - 1) ↔
          antiRecurrenceComplement a ((n + 1) * a.length) =
            antiRecurrenceComplement a (n * a.length + 1) + (a.length - 1)) →
        antiRecurrence a n + a.length * a.sum < antiRecurrence a (n + 1))

Sources

• Robbert Fokkink and Gandhar Joshi, Anti-Recurrence Sequences, INTEGERS 26 (2026), Article A24, Lemma 1.

Uses 2

Statement usesAnti-recurrence numbers · Non-anti-recurrence numbers

TheoremCharacterization of anti-recurrence sequences#●ready to prove

Let \(a = (a_1, \dots, a_k)\) be a linear form with positive integer coefficients and \(k > 1\), with anti-recurrence numbers \(A_1, A_2, \dots\) and non-anti-recurrence numbers \(B_1, B_2, \dots\). Let \((x_i)_{i \ge 0}\) and \((y_i)_{i \ge 0}\) be sequences of natural numbers. Then \(x\) and \(y\) are strictly increasing, every \(y_i\) is positive, every positive integer is a term of exactly one of \(x\) and \(y\), and \(x_i = \sum_{j=1}^{k} a_j y_{ik+j-1}\) for all \(i\), if and only if \(x_i = A_{i+1}\) and \(y_i = B_{i+1}\) for all \(i\).

public theorem_wanted antiRecurrence_unique (a : List ℕ) (ha : ∀ x ∈ a, 0 < x)
    (hk : 1 < a.length) (A B : ℕ → ℕ) :
    (StrictMono A ∧ StrictMono B ∧ (∀ i, 0 < B i) ∧
        (∀ m, 0 < m → (m ∈ Set.range A ↔ m ∉ Set.range B)) ∧
        ∀ i, A i = ∑ j : Fin a.length, a[j] * B (i * a.length + j)) ↔
      (A = fun i => antiRecurrence a (i + 1)) ∧ B = fun i => antiRecurrenceComplement a (i + 1)

Sources

• Robbert Fokkink and Gandhar Joshi, Anti-Recurrence Sequences, INTEGERS 26 (2026), Article A24, Lemma 2.

Uses 2

Statement usesAnti-recurrence numbers · Non-anti-recurrence numbers

TheoremIntervals and residues of the anti-\(k\)-bonacci numbers#●ready to prove

Let \(k > 1\), let \(A_n\) be the anti-recurrence numbers of the linear form \((1, \dots, 1)\) of length \(k\), and put \(i = \lfloor k/2 \rfloor\) and \(\kappa = k^2 + 1\). Then for every \(n \ge 1\), \(A_n\) lies in the interval \([\kappa(n - 1) + 1, \kappa n]\), and \(A_n \equiv ik + c \pmod{\kappa}\) for some natural number \(c\) with \(1 \le c \le k\) if \(k\) is even and \(i + 1 \le c \le i + k\) if \(k\) is odd.

The paper attaches the condition \(k > 2\) to \(\kappa\); it is not needed, since \(k = 2\) is the anti-Fibonacci case (Zaslavsky's formula \(A_n = 5n - 2 + PD_{n-1}\), with \(PD\) the period-doubling sequence).

public theorem_wanted antiBonacci_mem_Icc_and_modEq (k : ℕ) (hk : 1 < k) {n : ℕ} (hn : 1 ≤ n) :
    antiRecurrence (List.replicate k 1) n ∈ Finset.Icc ((k ^ 2 + 1) * (n - 1) + 1) ((k ^ 2 + 1) * n) ∧
      ∃ c : ℕ, (if Even k then 1 ≤ c ∧ c ≤ k else k / 2 + 1 ≤ c ∧ c ≤ k / 2 + k) ∧
        antiRecurrence (List.replicate k 1) n ≡ k / 2 * k + c [MOD k ^ 2 + 1]

Sources

• Robbert Fokkink and Gandhar Joshi, Anti-Recurrence Sequences, INTEGERS 26 (2026), Article A24, Lemma 3.

Uses 1

Statement usesAnti-recurrence numbers

TheoremLower bound for the first anti-recurrence number#●ready to prove

Let \(a = (a_1, \dots, a_k)\) be a linear form with positive integer coefficients, of trace \(\tau = a_1 + \dots + a_k\), and let \(A_1\) be its first anti-recurrence number. Then \(\tau + (k - 1)k/2 \le A_1\), and the inequality is strict if and only if \(a_j > 1\) for some \(j\) with \(2 \le j \le k\).

This corrects the printed strictness condition ("\(k > 2\) and not anti-bonacci"), which fails for \(a = (2, 1, 1)\): there \(A_1 = 2 + 2 + 3 = 7 = \tau + 3\). The correction follows the paper's proof, \(A_1 = \tau + \sum_j (j - 1) a_j\). The paper's hypothesis \(k > 1\) is not needed.

public theorem_wanted antiRecurrence_one_ge (a : List ℕ) (ha : ∀ x ∈ a, 0 < x) :
    a.sum + (a.length - 1) * a.length / 2 ≤ antiRecurrence a 1 ∧
      (a.sum + (a.length - 1) * a.length / 2 < antiRecurrence a 1 ↔
        ∃ j : Fin a.length, 1 ≤ (j : ℕ) ∧ 1 < a[j])

Sources

• Robbert Fokkink and Gandhar Joshi, Anti-Recurrence Sequences, INTEGERS 26 (2026), Article A24, Lemma 4.

Uses 1

Statement usesAnti-recurrence numbers

TheoremInterval location of anti-recurrence numbers for bounded forms#●ready to prove

Let \(a = (a_1, \dots, a_k)\) be a linear form with positive integer coefficients and \(k > 1\), of trace \(\tau = a_1 + \dots + a_k\), with anti-recurrence numbers \(A_1, A_2, \dots\) and non-anti-recurrence numbers \(B_1, B_2, \dots\), and let \(\kappa = k\tau + 1\). Suppose that \(a\) is \(A_1\)-bounded, that is, \(A_1 \le (k - 1)\tau + 2\). Then for every \(n \ge 1\), \(A_n\) lies in the interval \(I_n = [\kappa(n - 1) + 1, \kappa n]\), and the first \(k\) numbers of \(I_n\) are non-anti-recurrence numbers: \(B_{(n-1)k\tau + j} = \kappa(n - 1) + j\) for \(1 \le j \le k\).

public theorem_wanted antiRecurrence_mem_Icc_of_bounded (a : List ℕ) (ha : ∀ x ∈ a, 0 < x)
    (hk : 1 < a.length) (hb : antiRecurrence a 1 ≤ (a.length - 1) * a.sum + 2) {n : ℕ}
    (hn : 1 ≤ n) :
    antiRecurrence a n ∈
        Finset.Icc ((a.length * a.sum + 1) * (n - 1) + 1) ((a.length * a.sum + 1) * n) ∧
      ∀ j < a.length, antiRecurrenceComplement a ((n - 1) * a.length * a.sum + j + 1) =
        (a.length * a.sum + 1) * (n - 1) + j + 1

Sources

• Robbert Fokkink and Gandhar Joshi, Anti-Recurrence Sequences, INTEGERS 26 (2026), Article A24, Lemma 5.

Uses 2

Statement usesAnti-recurrence numbers · Non-anti-recurrence numbers

TheoremKimberling's bounds for the anti-Pell numbers#●ready to prove

Let \(A_n\) be the anti-recurrence numbers of the linear form \(a = (1, 2)\) (the anti-Pell numbers), let \(B_m\) be its non-anti-recurrence numbers, and put \(B^1_n = B_{2n-1}\) and \(B^2_n = B_{2n}\). Then for every \(n \ge 1\) we have \(0 \le A_n - 7n + 3 \le 2\), \(0 \le 3B^1_n - 7n + 6 \le 3\) and \(0 \le 3B^2_n - 7n + 2 \le 3\).

public theorem_wanted antiPell_kimberling_bounds {n : ℕ} (hn : 1 ≤ n) :
    (0 ≤ (antiRecurrence [1, 2] n : ℤ) - 7 * n + 3 ∧
        (antiRecurrence [1, 2] n : ℤ) - 7 * n + 3 ≤ 2) ∧
      (0 ≤ 3 * (antiRecurrenceComplement [1, 2] (2 * n - 1) : ℤ) - 7 * n + 6 ∧
        3 * (antiRecurrenceComplement [1, 2] (2 * n - 1) : ℤ) - 7 * n + 6 ≤ 3) ∧
      (0 ≤ 3 * (antiRecurrenceComplement [1, 2] (2 * n) : ℤ) - 7 * n + 2 ∧
        3 * (antiRecurrenceComplement [1, 2] (2 * n) : ℤ) - 7 * n + 2 ≤ 3)

Sources

• Robbert Fokkink and Gandhar Joshi, Anti-Recurrence Sequences, INTEGERS 26 (2026), Article A24, Theorem 1.

Uses 2

Statement usesAnti-recurrence numbers · Non-anti-recurrence numbers

TheoremKimberling's bounds for the anti-Jacobsthal numbers#●ready to prove

Let \(A_n\) be the anti-recurrence numbers of the linear form \(a = (2, 1)\) (the anti-Jacobsthal numbers), let \(B_m\) be its non-anti-recurrence numbers, and put \(B^1_n = B_{2n-1}\) and \(B^2_n = B_{2n}\). Then for every \(n \ge 1\) we have \(0 \le A_n - 7n + 4 \le 3\), \(0 \le 3B^1_n - 7n + 6 \le 4\) and \(0 \le 3B^2_n - 7n + 2 \le 3\).

public theorem_wanted antiJacobsthal_kimberling_bounds {n : ℕ} (hn : 1 ≤ n) :
    (0 ≤ (antiRecurrence [2, 1] n : ℤ) - 7 * n + 4 ∧
        (antiRecurrence [2, 1] n : ℤ) - 7 * n + 4 ≤ 3) ∧
      (0 ≤ 3 * (antiRecurrenceComplement [2, 1] (2 * n - 1) : ℤ) - 7 * n + 6 ∧
        3 * (antiRecurrenceComplement [2, 1] (2 * n - 1) : ℤ) - 7 * n + 6 ≤ 4) ∧
      (0 ≤ 3 * (antiRecurrenceComplement [2, 1] (2 * n) : ℤ) - 7 * n + 2 ∧
        3 * (antiRecurrenceComplement [2, 1] (2 * n) : ℤ) - 7 * n + 2 ≤ 3)

Sources

• Robbert Fokkink and Gandhar Joshi, Anti-Recurrence Sequences, INTEGERS 26 (2026), Article A24, Theorem 2.

Uses 2

Statement usesAnti-recurrence numbers · Non-anti-recurrence numbers

TheoremBounded anti-recurrence sequences are automatic up to a linear term#●ready to prove

Let \(a = (a_1, \dots, a_k)\) be a linear form with positive integer coefficients and \(k > 1\), of trace \(\tau = a_1 + \dots + a_k\), with anti-recurrence numbers \(A_1, A_2, \dots\), and let \(\kappa = k\tau + 1\). If \(a\) is \(A_1\)-bounded, that is, \(A_1 \le (k - 1)\tau + 2\), then the integer sequence \(n \mapsto A_{n+1} - \kappa(n + 1)\), indexed from \(n = 0\), is \(\tau\)-automatic: \(\tau \ge 2\) and its \(\tau\)-kernel is finite.

Automaticity is stated through Eilenberg's characterization by a finite kernel, in place of the paper's definition by a finite automaton with output.

public theorem_wanted antiRecurrence_sub_isKAutomatic_of_bounded (a : List ℕ)
    (ha : ∀ x ∈ a, 0 < x) (hk : 1 < a.length)
    (hb : antiRecurrence a 1 ≤ (a.length - 1) * a.sum + 2) :
    IsKAutomatic a.sum fun n =>
      (antiRecurrence a (n + 1) : ℤ) - (a.length * a.sum + 1) * (n + 1)

Sources

• Robbert Fokkink and Gandhar Joshi, Anti-Recurrence Sequences, INTEGERS 26 (2026), Article A24, Theorem 4.

Uses 2

Statement uses\(k\)-automatic sequence (finite-kernel definition) · Anti-recurrence numbers

42 fully proved21 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.