Complementary sequences

DefinitionComplementary pair of sequences#✓fully proved

Two sequences \(a, b : \mathbb{N} \to \mathbb{N}\), indexed from \(0\), form a complementary pair when all their terms are positive, both are strictly increasing, no term of \(a\) equals a term of \(b\), and every positive integer is a term of \(a\) or a term of \(b\). In particular, the ranges of \(a\) and \(b\) partition the positive integers.

public def IsComplementaryPair (a b : ℕ → ℕ) : Prop :=
  (∀ n, 0 < a n) ∧ (∀ n, 0 < b n) ∧
    StrictMono a ∧ StrictMono b ∧
    (∀ m n, a m ≠ b n) ∧
    ∀ n, 0 < n → (∃ m, a m = n) ∨ (∃ m, b m = n)

Used by 3

Used byComplementary pair determined by \(a_n = b_{2n} + b_{4n}\) · Complementary pair determined by \(a_n = b_{hn} + b_{khn}\) · Complementary pair determined by \(a_n = b_{2n} + b_{4n} + 1\)

DefinitionThe subsequence-sum equation \(a_n = b_{hn} + b_{khn}\)#✓fully proved

Sequences \(a, b : \mathbb{N} \to \mathbb{N}\) and natural numbers \(h\) and \(k\) satisfy the parametrized subsequence-sum equation when \(h \ge 2\), \(k \ge 2\), \(b_0 = 1\), and \(a_n = b_{hn} + b_{khn}\) for every \(n \in \mathbb{N}\).

public def SatisfiesParametrizedSumEquation (a b : ℕ → ℕ) (h k : ℕ) : Prop :=
  2 ≤ h ∧ 2 ≤ k ∧ b 0 = 1 ∧ ∀ n, a n = b (h * n) + b (k * h * n)

Used by 1

Used byComplementary pair determined by \(a_n = b_{hn} + b_{khn}\)

DefinitionThe subsequence-sum equation \(a_n = b_{2n} + b_{4n}\)#✓fully proved

Sequences \(a, b : \mathbb{N} \to \mathbb{N}\) satisfy this equation when \(b_0 = 1\) and \(a_n = b_{2n} + b_{4n}\) for every \(n \in \mathbb{N}\).

public def SatisfiesBaseSumEquation (a b : ℕ → ℕ) : Prop :=
  b 0 = 1 ∧ ∀ n, a n = b (2 * n) + b (4 * n)

Used by 1

Used byComplementary pair determined by \(a_n = b_{2n} + b_{4n}\)

DefinitionThe subsequence-sum equation \(a_n = b_{2n} + b_{4n} + 1\)#✓fully proved

Sequences \(a, b : \mathbb{N} \to \mathbb{N}\) satisfy this equation when \(b_0 = 1\) and \(a_n = b_{2n} + b_{4n} + 1\) for every \(n \in \mathbb{N}\).

public def SatisfiesShiftedSumEquation (a b : ℕ → ℕ) : Prop :=
  b 0 = 1 ∧ ∀ n, a n = b (2 * n) + b (4 * n) + 1

Used by 1

Used byComplementary pair determined by \(a_n = b_{2n} + b_{4n} + 1\)

DefinitionComplementary pair determined by \(a_n = b_{hn} + b_{khn}\)#✓fully proved

Sequences \(a, b : \mathbb{N} \to \mathbb{N}\) form a complementary pair determined by this equation with natural-number parameters \(h\) and \(k\) when they form a complementary pair (both strictly increasing with positive terms, and every positive integer is a term of exactly one of them), \(h \ge 2\), \(k \ge 2\), \(b_0 = 1\), and \(a_n = b_{hn} + b_{khn}\) for every \(n \in \mathbb{N}\).

public def IsComplementaryDeterminedByParametrizedSumEquation
    (a b : ℕ → ℕ) (h k : ℕ) : Prop :=
  IsComplementaryPair a b ∧ SatisfiesParametrizedSumEquation a b h k

Uses 2

Statement usesComplementary pair of sequences · The subsequence-sum equation \(a_n = b_{hn} + b_{khn}\)

DefinitionComplementary pair determined by \(a_n = b_{2n} + b_{4n}\)#✓fully proved

Sequences \(a, b : \mathbb{N} \to \mathbb{N}\) form a complementary pair determined by this equation when they form a complementary pair (both strictly increasing with positive terms, and every positive integer is a term of exactly one of them) and they satisfy \(b_0 = 1\) and \(a_n = b_{2n} + b_{4n}\) for every \(n \in \mathbb{N}\).

public def IsComplementaryDeterminedByBaseSumEquation (a b : ℕ → ℕ) : Prop :=
  IsComplementaryPair a b ∧ SatisfiesBaseSumEquation a b

Uses 2

Statement usesComplementary pair of sequences · The subsequence-sum equation \(a_n = b_{2n} + b_{4n}\)

DefinitionComplementary pair determined by \(a_n = b_{2n} + b_{4n} + 1\)#✓fully proved

Sequences \(a, b : \mathbb{N} \to \mathbb{N}\) form a complementary pair determined by this equation when they form a complementary pair (both strictly increasing with positive terms, and every positive integer is a term of exactly one of them) and they satisfy \(b_0 = 1\) and \(a_n = b_{2n} + b_{4n} + 1\) for every \(n \in \mathbb{N}\).

public def IsComplementaryDeterminedByShiftedSumEquation (a b : ℕ → ℕ) : Prop :=
  IsComplementaryPair a b ∧ SatisfiesShiftedSumEquation a b

Uses 2

Statement usesComplementary pair of sequences · The subsequence-sum equation \(a_n = b_{2n} + b_{4n} + 1\)

DefinitionThe \(n\)-th non-value of a sequence#✓fully proved

For \(f : \mathbb{N} \to \mathbb{N}\) and \(n \ge 1\), the \(n\)-th non-value of \(f\) is the \(n\)-th smallest positive integer that is not of the form \(f(m)\) with \(m \ge 1\), or \(0\) if fewer than \(n\) such integers exist. At \(n = 0\) it takes the same value as at \(n = 1\).

In the paper's notation, where \(f = f_{\neg P}\) lists the positive integers without a property \(P\), the \(n\)-th non-value of \(f\) is \(f_P(n)\), the \(n\)-th term of the complementary sequence.

public noncomputable def nthNonValue (f : ℕ → ℕ) (n : ℕ) : ℕ :=
  Nat.nth (fun x => 0 < x ∧ ∀ m, 1 ≤ m → f m ≠ x) (n - 1)

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Section 1 (definition of f_P).

Used by 22

Used byIntegers not of the form \(m + 1^k + \cdots + m^k\) · Complementary sequences from an interleaving function · Interleaving formula when \(f(m) - \alpha(m) \ge m\) · Interleaving formula when \(f(m) - \alpha(m) < m\) · Complementary sequences from one evaluation of the counting function · Complementary sequences in two Lambek–Moser steps · Formula for the non-polygonal numbers · Rounding formula for the non-\(k\)-gonal numbers, \(3 \le k \le 10\) · Rounding formula for the non-\(k\)-gonal numbers, every \(k \ge 3\) · Shifted formula for the non-polygonal numbers · Formula for the non-pyramidal numbers · Two-case formula for the non-pyramidal numbers when \(k \le 5\) · Two-case formula for the non-pyramidal numbers when \(k \le 8\) · Formula for the non-second-pentagonal numbers · Formula for the non-second-polygonal numbers · Formula for the non-simplex numbers · Formula for the non-simplex numbers when \(k \le 15\) · Formula for the non-square numbers · The first non-square · The second non-square · Integers missed by the sums \(1^k + \dots + j^k\) · Formula for the \(n\)-th non-triangular number

TheoremThe first non-square#✓fully proved

The smallest positive integer that is not the square of a positive integer is \(2\); that is, the first non-value of \(m \mapsto m^2\) is \(2\).

public theorem nthNonValue_sq_one : nthNonValue (fun m => m ^ 2) 1 = 2

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Section 1 (the non-squares).

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremThe second non-square#✓fully proved

The second smallest positive integer that is not the square of a positive integer is \(3\); that is, the second non-value of \(m \mapsto m^2\) is \(3\).

public theorem nthNonValue_sq_two : nthNonValue (fun m => m ^ 2) 2 = 3

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Section 1 (the non-squares).

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremComplementary sequences in two Lambek–Moser steps#●ready to prove

Let \(f : \mathbb{N} \to \mathbb{N}\) satisfy \(f(1) \ge 1\) and \(f(m + 1) \ge f(m) + m\) for all \(m \ge 1\), let \(C(x)\) be the number of \(m\) with \(1 \le m \le x\) and \(f(m) \le x\), and for \(n \ge 1\) let \(f_P(n)\) be the \(n\)-th positive integer that is not a value \(f(m)\) with \(m \ge 1\). Then \(f_P(n) = n + C(n + C(n))\) for every \(n \ge 1\).

Under the hypotheses, \(f(m) \ge m\) for all \(m \ge 1\), so \(C(x)\) is the number of all \(m \ge 1\) with \(f(m) \le x\), the counting function of the values of \(f\).

public theorem_wanted nthNonValue_eq_two_step (f : ℕ → ℕ) (hf1 : 1 ≤ f 1)
    (hgap : ∀ m, 1 ≤ m → f m + m ≤ f (m + 1)) (n : ℕ) (hn : 1 ≤ n) :
    let C : ℕ → ℕ := fun x => ((Finset.Icc 1 x).filter (fun m => f m ≤ x)).card
    nthNonValue f n = n + C (n + C n)

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Theorem 1.

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremComplementary sequences from one evaluation of the counting function#●ready to prove

Let \(f : \mathbb{N} \to \mathbb{N}\) satisfy \(f(1) \ge 1\) and \(f(m + 1) \ge f(m) + m\) for all \(m \ge 1\), let \(C(x)\) be the number of \(m\) with \(1 \le m \le x\) and \(f(m) \le x\), and for \(n \ge 1\) let \(f_P(n)\) be the \(n\)-th positive integer that is not a value \(f(m)\) with \(m \ge 1\). Then for every \(n \ge 1\), \(f_P(n) = n + C(n) + 1\) if \(f(C(n) + 1) \le n + C(n)\), and \(f_P(n) = n + C(n)\) otherwise.

public theorem_wanted nthNonValue_eq_one_step (f : ℕ → ℕ) (hf1 : 1 ≤ f 1)
    (hgap : ∀ m, 1 ≤ m → f m + m ≤ f (m + 1)) (n : ℕ) (hn : 1 ≤ n) :
    let C : ℕ → ℕ := fun x => ((Finset.Icc 1 x).filter (fun m => f m ≤ x)).card
    nthNonValue f n = if f (C n + 1) ≤ n + C n then n + C n + 1 else n + C n

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Theorem 2.

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremComplementary sequences from an interleaving function#●ready to prove

Let \(f : \mathbb{N} \to \mathbb{N}\) satisfy \(f(1) \ge 1\) and \(f(m + 1) \ge f(m) + m\) for all \(m \ge 1\), and for \(n \ge 1\) let \(f_P(n)\) be the \(n\)-th positive integer that is not a value \(f(m)\) with \(m \ge 1\). Let \(\alpha : \mathbb{N} \to \mathbb{R}\) satisfy \(f(m - 1) \le \alpha(m) \le f(m)\) for all \(m \ge 2\), and let \(h : \mathbb{N} \to \mathbb{N}\) satisfy \(h(n) \ge 1\) and \(\alpha(h(n)) \le n < \alpha(h(n) + 1)\) for all \(n \ge 1\). Then for every \(n \ge 1\), \(f_P(n) = n + h(n) + 1\) if \(f(h(n) + 1) \le n + h(n)\); otherwise \(f_P(n) = n + h(n) - 1\) if \(n + h(n) \le f(h(n))\), and \(f_P(n) = n + h(n)\) if not.

For increasing \(\alpha\) with \(\alpha(1) = 1\), the paper's choice of \(h(n)\) as the largest \(m \ge 1\) with \(\alpha(m) \le n\) satisfies the hypothesis on \(h\).

public theorem_wanted nthNonValue_eq_interleave (f : ℕ → ℕ) (hf1 : 1 ≤ f 1)
    (hgap : ∀ m, 1 ≤ m → f m + m ≤ f (m + 1)) (α : ℕ → ℝ)
    (hα : ∀ m, 2 ≤ m → (f (m - 1) : ℝ) ≤ α m ∧ α m ≤ f m) (h : ℕ → ℕ)
    (hh : ∀ n, 1 ≤ n → 1 ≤ h n ∧ α (h n) ≤ n ∧ (n : ℝ) < α (h n + 1)) (n : ℕ) (hn : 1 ≤ n) :
    nthNonValue f n =
      if f (h n + 1) ≤ n + h n then n + h n + 1
      else if n + h n ≤ f (h n) then n + h n - 1
      else n + h n

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Theorem 3.

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremInterleaving formula when \(f(m) - \alpha(m) < m\)#●ready to prove

Let \(f : \mathbb{N} \to \mathbb{N}\) satisfy \(f(1) \ge 1\) and \(f(m + 1) \ge f(m) + m\) for all \(m \ge 1\), and for \(n \ge 1\) let \(f_P(n)\) be the \(n\)-th positive integer that is not a value \(f(m)\) with \(m \ge 1\). Let \(\alpha : \mathbb{N} \to \mathbb{R}\) satisfy \(f(m - 1) \le \alpha(m) \le f(m)\) for all \(m \ge 2\), and let \(h : \mathbb{N} \to \mathbb{N}\) satisfy \(h(n) \ge 1\) and \(\alpha(h(n)) \le n < \alpha(h(n) + 1)\) for all \(n \ge 1\). Suppose moreover that \(f(m) - \alpha(m) < m\) for all \(m \ge 1\). Then for every \(n \ge 1\), \(f_P(n) = n + h(n) + 1\) if \(f(h(n) + 1) \le n + h(n)\), and \(f_P(n) = n + h(n)\) otherwise.

public theorem_wanted nthNonValue_eq_interleave_of_sub_lt (f : ℕ → ℕ) (hf1 : 1 ≤ f 1)
    (hgap : ∀ m, 1 ≤ m → f m + m ≤ f (m + 1)) (α : ℕ → ℝ)
    (hα : ∀ m, 2 ≤ m → (f (m - 1) : ℝ) ≤ α m ∧ α m ≤ f m) (h : ℕ → ℕ)
    (hh : ∀ n, 1 ≤ n → 1 ≤ h n ∧ α (h n) ≤ n ∧ (n : ℝ) < α (h n + 1))
    (hclose : ∀ m : ℕ, 1 ≤ m → (f m : ℝ) - α m < m) (n : ℕ) (hn : 1 ≤ n) :
    nthNonValue f n = if f (h n + 1) ≤ n + h n then n + h n + 1 else n + h n

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Corollary 1.

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremInterleaving formula when \(f(m) - \alpha(m) \ge m\)#●ready to prove

Let \(f : \mathbb{N} \to \mathbb{N}\) satisfy \(f(1) \ge 1\) and \(f(m + 1) \ge f(m) + m\) for all \(m \ge 1\), and for \(n \ge 1\) let \(f_P(n)\) be the \(n\)-th positive integer that is not a value \(f(m)\) with \(m \ge 1\). Let \(\alpha : \mathbb{N} \to \mathbb{R}\) satisfy \(f(m - 1) \le \alpha(m) \le f(m)\) for all \(m \ge 2\), and let \(h : \mathbb{N} \to \mathbb{N}\) satisfy \(h(n) \ge 1\) and \(\alpha(h(n)) \le n < \alpha(h(n) + 1)\) for all \(n \ge 1\). Suppose moreover that \(f(m) - \alpha(m) \ge m\) for all \(m \ge 2\). Then for every \(n \ge 1\), \(f_P(n) = n + h(n)\) if \(f(h(n)) < n + h(n)\), and \(f_P(n) = n + h(n) - 1\) otherwise.

public theorem_wanted nthNonValue_eq_interleave_of_le_sub (f : ℕ → ℕ) (hf1 : 1 ≤ f 1)
    (hgap : ∀ m, 1 ≤ m → f m + m ≤ f (m + 1)) (α : ℕ → ℝ)
    (hα : ∀ m, 2 ≤ m → (f (m - 1) : ℝ) ≤ α m ∧ α m ≤ f m) (h : ℕ → ℕ)
    (hh : ∀ n, 1 ≤ n → 1 ≤ h n ∧ α (h n) ≤ n ∧ (n : ℝ) < α (h n + 1))
    (hfar : ∀ m : ℕ, 2 ≤ m → (m : ℝ) ≤ f m - α m) (n : ℕ) (hn : 1 ≤ n) :
    nthNonValue f n = if f (h n) < n + h n then n + h n else n + h n - 1

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Corollary 2.

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremFormula for the \(n\)-th non-triangular number#●ready to prove

For every integer \(n \ge 1\), the \(n\)-th smallest positive integer that is not a triangular number \(j(j+1)/2\) with \(j \ge 1\) is \(n + \lfloor \sqrt{2n} + 1/2 \rfloor\).

public theorem_wanted nthNonValue_triangular_eq_round (n : ℕ) (hn : 1 ≤ n) :
    nthNonValue (fun j => j * (j + 1) / 2) n = n + ⌊Real.sqrt (2 * n) + 1 / 2⌋₊

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Corollary 3.

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremFormula for the non-square numbers#●ready to prove

For every integer \(n \ge 1\), the \(n\)-th positive integer that is not a perfect square is \(n + \lfloor \sqrt{n} + 1/2 \rfloor\).

public theorem_wanted nthNonValue_sq_eq_round (n : ℕ) (hn : 1 ≤ n) :
    nthNonValue (fun j => j ^ 2) n = n + ⌊Real.sqrt n + 1 / 2⌋₊

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Corollary 3.

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremFormula for the non-polygonal numbers#●ready to prove

Let \(k \ge 3\), and for \(j \ge 1\) let \(T(k, j) = (k - 2) j (j - 1)/2 + j\) be the \(k\)-gonal numbers. For every integer \(n \ge 1\), put \(s = \lfloor \sqrt{2n/(k - 2)} \rfloor\). Then the \(n\)-th positive integer that is not of the form \(T(k, j)\) with \(j \ge 1\) equals \(n + s + 1\) if \((k - 2) s (s + 1) < 2n\), and \(n + s\) otherwise.

public theorem_wanted nthNonValue_polygonal (k : ℕ) (hk : 3 ≤ k) (n : ℕ) (hn : 1 ≤ n) :
    let s := Nat.sqrt (2 * n / (k - 2))
    nthNonValue (fun j => (k - 2) * j * (j - 1) / 2 + j) n =
      if (k - 2) * s * (s + 1) < 2 * n then n + s + 1 else n + s

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Theorem 4, Equation (3).

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremRounding formula for the non-\(k\)-gonal numbers, \(3 \le k \le 10\)#●ready to prove

Let \(3 \le k \le 10\); the \(k\)-gonal numbers are \((k - 2) j (j - 1)/2 + j\) for \(j \ge 1\). For every \(n \ge 1\), the \(n\)-th positive integer that is not a \(k\)-gonal number equals \(n + \lfloor \sqrt{2n/(k - 2)} + 1/2 \rfloor\).

public theorem_wanted nthNonValue_polygonal_eq_round (k : ℕ) (hk : 3 ≤ k) (hk' : k ≤ 10)
    (n : ℕ) (hn : 1 ≤ n) :
    nthNonValue (fun j => (k - 2) * j * (j - 1) / 2 + j) n =
      n + ⌊Real.sqrt (2 * n / ((k : ℝ) - 2)) + 1 / 2⌋₊

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Theorem 4 (last sentence).

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremShifted formula for the non-polygonal numbers#●ready to prove

Let \(k \ge 3\), let \(r\) be a real number with \(-1 \le r \le k - 4\), and for \(j \ge 1\) let \(T(k, j) = (k - 2) j (j - 1)/2 + j\) be the \(k\)-gonal numbers. For every integer \(n \ge 1\), put \(s = \lfloor \sqrt{(2n + r)/(k - 2)} \rfloor\). Then the \(n\)-th positive integer that is not of the form \(T(k, j)\) with \(j \ge 1\) equals \(n + s + 1\) if \((k - 2) s (s + 1) < 2n\), and \(n + s\) otherwise.

public theorem_wanted nthNonValue_polygonal_shift (k : ℕ) (hk : 3 ≤ k) (r : ℝ) (hr : -1 ≤ r)
    (hr' : r ≤ (k : ℝ) - 4) (n : ℕ) (hn : 1 ≤ n) :
    let s := ⌊Real.sqrt ((2 * n + r) / ((k : ℝ) - 2))⌋₊
    nthNonValue (fun j => (k - 2) * j * (j - 1) / 2 + j) n =
      if (k - 2) * s * (s + 1) < 2 * n then n + s + 1 else n + s

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Theorem 5, Equation (4).

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremRounding formula for the non-\(k\)-gonal numbers, every \(k \ge 3\)#●ready to prove

Let \(k \ge 3\); the \(k\)-gonal numbers are \((k - 2) j (j - 1)/2 + j\) for \(j \ge 1\). For every \(n \ge 1\), the \(n\)-th positive integer that is not a \(k\)-gonal number equals \(n + \lfloor \sqrt{(2n - 2 + \lfloor (k + 1)/4 \rfloor)/(k - 2)} + 1/2 \rfloor\).

This corresponds to the shift \(r = \lfloor (k + 1)/4 \rfloor - 2\) in the source.

public theorem_wanted nthNonValue_polygonal_eq_round_shift (k : ℕ) (hk : 3 ≤ k) (n : ℕ)
    (hn : 1 ≤ n) :
    nthNonValue (fun j => (k - 2) * j * (j - 1) / 2 + j) n =
      n + ⌊Real.sqrt ((2 * n - 2 + ((k + 1) / 4 : ℕ)) / ((k : ℝ) - 2)) + 1 / 2⌋₊

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Theorem 5 (last sentence).

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremFormula for the non-second-pentagonal numbers#●ready to prove

For every integer \(n \ge 1\), put \(s = \lfloor \sqrt{2n/3} \rfloor\). Then the \(n\)-th positive integer that is not a second pentagonal number \((3j^2 + j)/2\) with \(j \ge 1\) equals \(n + s + 1\) if \(s (3s + 5) + 4 \le 2n\), and \(n + s\) otherwise.

public theorem_wanted nthNonValue_secondPentagonal (n : ℕ) (hn : 1 ≤ n) :
    let s := Nat.sqrt (2 * n / 3)
    nthNonValue (fun j => (3 * j ^ 2 + j) / 2) n =
      if s * (3 * s + 5) + 4 ≤ 2 * n then n + s + 1 else n + s

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Theorem 6.

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremFormula for the non-second-polygonal numbers#●ready to prove

Let \(k > 5\), and for \(j \ge 1\) let \(S(k, j) = ((k - 2) j^2 + (k - 4) j)/2\) be the second \(k\)-gonal numbers. For every integer \(n \ge 1\), put \(s = \lfloor \sqrt{2n/(k - 2)} \rfloor\). Then the \(n\)-th positive integer that is not of the form \(S(k, j)\) with \(j \ge 1\) equals \(n + s\) if \((k - 2) s (s + 1) < 2n + 4s\), and \(n + s - 1\) otherwise.

public theorem_wanted nthNonValue_secondPolygonal (k : ℕ) (hk : 5 < k) (n : ℕ) (hn : 1 ≤ n) :
    let s := Nat.sqrt (2 * n / (k - 2))
    nthNonValue (fun j => ((k - 2) * j ^ 2 + (k - 4) * j) / 2) n =
      if (k - 2) * s * (s + 1) < 2 * n + 4 * s then n + s else n + s - 1

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Theorem 7, Equation (5).

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremNon-centered polygonal numbers#●ready to prove

Let \(k \ge 3\); the centered \(k\)-gonal numbers are \(k j (j + 1)/2 + 1\) for \(j \ge 0\). For \(n \ge 1\) let \(a(n)\) be the \(n\)-th nonnegative integer that is not a centered \(k\)-gonal number (so \(a(1) = 0\)), and let \(s = \lfloor \sqrt{2n/k} \rfloor\). Then \(a(n) = n + s\) if \(k s (s + 1) < 2(n + s - 1)\), and \(a(n) = n + s - 1\) otherwise.

public theorem_wanted nth_nonCenteredPolygonal (k : ℕ) (hk : 3 ≤ k) (n : ℕ) (hn : 1 ≤ n) :
    let s := Nat.sqrt (2 * n / k)
    Nat.nth (fun x => ∀ j, k * j * (j + 1) / 2 + 1 ≠ x) (n - 1) =
      if k * s * (s + 1) < 2 * (n + s - 1) then n + s else n + s - 1

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Theorem 8.

TheoremFormula for the non-pyramidal numbers#●ready to prove

Let \(3 \le k \le 8\), and for \(j \ge 1\) let \(P(k, j) = j (j + 1) ((k - 2) j - (k - 5))/6\) be the \(k\)-gonal pyramidal numbers. For every integer \(n \ge 1\), put \(s = \lfloor \sqrt[3]{6n/(k - 2)} \rfloor\). Then the \(n\)-th positive integer that is not of the form \(P(k, j)\) with \(j \ge 1\) equals \(n + s + 1\) if \(6n \ge s^3 (k - 2) + 3 s^2 (k - 1) + s (2k - 1) + 6\); otherwise it equals \(n + s - 1\) if \(6n \le s (s - 1) (s (k - 2) + k + 1)\), and \(n + s\) if not.

public theorem_wanted nthNonValue_pyramidal (k : ℕ) (hk : 3 ≤ k) (hk' : k ≤ 8) (n : ℕ)
    (hn : 1 ≤ n) :
    let s := Nat.nthRoot 3 (6 * n / (k - 2))
    nthNonValue (fun j => j * (j + 1) * ((k - 2) * j + 5 - k) / 6) n =
      if s ^ 3 * (k - 2) + 3 * s ^ 2 * (k - 1) + s * (2 * k - 1) + 6 ≤ 6 * n then n + s + 1
      else if 6 * n ≤ s * (s - 1) * (s * (k - 2) + k + 1) then n + s - 1
      else n + s

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Theorem 9, Equation (6).

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremTwo-case formula for the non-pyramidal numbers when \(k \le 5\)#●ready to prove

Let \(3 \le k \le 5\), and for \(j \ge 1\) let \(P(k, j) = j (j + 1) ((k - 2) j - (k - 5))/6\) be the \(k\)-gonal pyramidal numbers. For every integer \(n \ge 1\), put \(s = \lfloor \sqrt[3]{6n/(k - 2)} \rfloor\). Then the \(n\)-th positive integer that is not of the form \(P(k, j)\) with \(j \ge 1\) equals \(n + s - 1\) if \(6n \le s (s - 1) (s (k - 2) + k + 1)\), and \(n + s\) otherwise.

public theorem_wanted nthNonValue_pyramidal_two_case (k : ℕ) (hk : 3 ≤ k) (hk' : k ≤ 5)
    (n : ℕ) (hn : 1 ≤ n) :
    let s := Nat.nthRoot 3 (6 * n / (k - 2))
    nthNonValue (fun j => j * (j + 1) * ((k - 2) * j + 5 - k) / 6) n =
      if 6 * n ≤ s * (s - 1) * (s * (k - 2) + k + 1) then n + s - 1 else n + s

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Corollary 4, Equation (7).

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremTwo-case formula for the non-pyramidal numbers when \(k \le 8\)#●ready to prove

Let \(3 \le k \le 8\), and for \(j \ge 1\) let \(P(k, j) = j (j + 1) ((k - 2) j - (k - 5))/6\) be the \(k\)-gonal pyramidal numbers. For every integer \(n \ge 1\), put \(s = \lfloor \sqrt[3]{6n/(k - 2)} \rfloor\). Then the \(n\)-th positive integer that is not of the form \(P(k, j)\) with \(j \ge 1\) equals \(n + s - 1\) if \(6n \le s (s - 1) (s (k - 2) + k + 1)\), and \(n + s\) otherwise.

This extends Equation (7) of Corollary 4 from \(k \le 5\) to \(k \le 8\); the paper reports it after checking small values of \(n\).

public theorem_wanted nthNonValue_pyramidal_two_case_le_eight (k : ℕ) (hk : 3 ≤ k)
    (hk' : k ≤ 8) (n : ℕ) (hn : 1 ≤ n) :
    let s := Nat.nthRoot 3 (6 * n / (k - 2))
    nthNonValue (fun j => j * (j + 1) * ((k - 2) * j + 5 - k) / 6) n =
      if 6 * n ≤ s * (s - 1) * (s * (k - 2) + k + 1) then n + s - 1 else n + s

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, remark after Corollary 4.

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremIntegers missed by the sums \(1^k + \dots + j^k\)#●ready to prove

Let \(k > 1\) and \(n \ge 1\) be integers, and let \(h = \lfloor ((k+1)n)^{1/(k+1)} \rfloor\). Then the \(n\)-th smallest positive integer that is not of the form \(\sum_{i=1}^{j} i^k\) with \(j \ge 1\) is \(n + h - 1\) if \(n \le \sum_{i=1}^{h} (i^k - 1)\), and \(n + h\) otherwise.

public theorem_wanted nthNonValue_sumPow (k : ℕ) (hk : 1 < k) (n : ℕ) (hn : 1 ≤ n) :
    let h := Nat.nthRoot (k + 1) ((k + 1) * n)
    nthNonValue (fun j => ∑ i ∈ Finset.Icc 1 j, i ^ k) n =
      if n ≤ ∑ i ∈ Finset.Icc 1 h, (i ^ k - 1) then n + h - 1 else n + h

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Theorem 10 (third equivalent form).

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremIntegers not of the form \(m + 1^k + \cdots + m^k\)#●ready to prove

Let \(k > 1\). For \(n \ge 1\) let \(a(n)\) be the \(n\)-th positive integer that is not of the form \(m + \sum_{i=1}^m i^k\) with \(m \ge 1\), and let \(h = \lfloor ((k + 1) n)^{1/(k+1)} \rfloor\). Then \(a(n) = n + h - 1\) if \(n \le \sum_{i=1}^h i^k\), and \(a(n) = n + h\) otherwise.

public theorem_wanted nthNonValue_add_sumPow (k : ℕ) (hk : 1 < k) (n : ℕ) (hn : 1 ≤ n) :
    let h := Nat.nthRoot (k + 1) ((k + 1) * n)
    nthNonValue (fun j => j + ∑ i ∈ Finset.Icc 1 j, i ^ k) n =
      if n ≤ ∑ i ∈ Finset.Icc 1 h, i ^ k then n + h - 1 else n + h

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Theorem 11 (third equivalent form).

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremRising factorial between consecutive \(k\)-th powers#●ready to prove

Let \(k\) and \(n\) be natural numbers, write \(n^{\overline{k}} = n (n + 1) \cdots (n + k - 1)\) for the rising factorial, and let \(r = \lfloor (k^2 - 4k + 6)/4 \rfloor\) if \(k\) is even and \(r = \lfloor (k^2 - 6k + 11)/4 \rfloor\) if \(k\) is odd. If \(n \ge r\), then \((n + \lfloor k/2 \rfloor - 1)^k \le n^{\overline{k}} \le (n + \lfloor k/2 \rfloor)^k\).

Both numerators are positive: \(k^2 - 4k + 6 = (k - 2)^2 + 2\) and \(k^2 - 6k + 11 = (k - 3)^2 + 2\).

public theorem_wanted ascFactorial_bounds_half (k n : ℕ)
    (hn : (if Even k then (k ^ 2 + 6 - 4 * k) / 4 else (k ^ 2 + 11 - 6 * k) / 4) ≤ n) :
    (n + k / 2 - 1) ^ k ≤ n.ascFactorial k ∧ n.ascFactorial k ≤ (n + k / 2) ^ k

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Lemma 1, Equation (8).

TheoremFormula for the non-simplex numbers#●ready to prove

Let \(k\) satisfy \(1 < k \le 5\), \(k = 7\) or \(k = 9\). For every integer \(n \ge 1\), put \(R = \lfloor (k!\, n)^{1/k} \rfloor\) and let \(t = n + R - \lfloor k/2 \rfloor\), an integer. Then the \(n\)-th positive integer that is not a \(k\)-simplex number \(\binom{j + k - 1}{k}\) with \(j \ge 1\) equals \(t + 2\) if \(\binom{R + \lceil k/2 \rceil + 1}{k} \le t + 1\); otherwise it equals \(t\) if \(t < \binom{R + \lceil k/2 \rceil}{k}\), and \(t + 1\) if not.

public theorem_wanted nthNonValue_simplex (k : ℕ) (hk : 1 < k ∧ k ≤ 5 ∨ k = 7 ∨ k = 9) (n : ℕ)
    (hn : 1 ≤ n) :
    let R := Nat.nthRoot k (k.factorial * n)
    let t : ℤ := n + R - (k / 2 : ℕ)
    (nthNonValue (fun j => (j + k - 1).choose k) n : ℤ) =
      if ((R + (k + 1) / 2 + 1).choose k : ℤ) ≤ t + 1 then t + 2
      else if t < ((R + (k + 1) / 2).choose k : ℤ) then t
      else t + 1

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Theorem 12, Equation (9).

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

TheoremFormula for the non-simplex numbers when \(k \le 15\)#●ready to prove

Let \(1 < k \le 15\). For every integer \(n \ge 1\), put \(R = \lfloor (k!\, n)^{1/k} \rfloor\) and let \(t = n + R - \lfloor k/2 \rfloor\), an integer. Then the \(n\)-th positive integer that is not a \(k\)-simplex number \(\binom{j + k - 1}{k}\) with \(j \ge 1\) equals \(t + 2\) if \(\binom{R + \lceil k/2 \rceil + 1}{k} \le t + 1\); otherwise it equals \(t\) if \(t < \binom{R + \lceil k/2 \rceil}{k}\), and \(t + 1\) if not.

public theorem_wanted nthNonValue_simplex_le_fifteen (k : ℕ) (hk : 1 < k) (hk' : k ≤ 15) (n : ℕ)
    (hn : 1 ≤ n) :
    let R := Nat.nthRoot k (k.factorial * n)
    let t : ℤ := n + R - (k / 2 : ℕ)
    (nthNonValue (fun j => (j + k - 1).choose k) n : ℤ) =
      if ((R + (k + 1) / 2 + 1).choose k : ℤ) ≤ t + 1 then t + 2
      else if t < ((R + (k + 1) / 2).choose k : ℤ) then t
      else t + 1

Sources

• Chai Wah Wu, Algorithms for Complementary Sequences, INTEGERS 25 (2025), Article A95, Corollary 5.

Uses 1

Statement usesThe \(n\)-th non-value of a sequence

10 fully proved22 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.