Comma sequences

DefinitionMost significant digit#✓fully proved

For natural numbers \(b\) and \(m\), let \(k\) be the base-\(b\) logarithm of \(m\) rounded down, that is, the largest \(k\) with \(b^k \le m\) when \(b \ge 2\) and \(m \ge 1\), and \(k = 0\) otherwise. The most significant digit of \(m\) in base \(b\) is \(\lfloor m / b^k \rfloor\). When \(b \ge 2\) and \(m \ge 1\) this is the leading digit of the base-\(b\) expansion of \(m\).

public def commaMsd (b m : Nat) : Nat :=
  m / b ^ Nat.log b m

Used by 2

Used byRecovering the parent of a comma-child · Comma candidate digits

DefinitionComma candidate digits#✓fully proved

Let \(b\) and \(n\) be natural numbers and let \(y\) be a digit with \(0 \le y < b\). Put \(m = n + b\,(n \bmod b) + y\), where \(n \bmod b\) is the remainder of \(n\) on division by \(b\). Then \(y\) is a comma candidate for \(n\) in base \(b\) if \(m > 0\) and the most significant base-\(b\) digit of \(m\) equals \(y\).

For such a candidate \(y\) in base \(b \ge 2\), the difference \(m - n = b\,(n \bmod b) + y\) is written with the base-\(b\) digits \(n \bmod b\) and \(y\): the last digit of \(n\) followed by the leading digit of \(m\).

public def IsCommaCandidate (b n : Nat) (y : Fin b) : Prop :=
  let m := n + b * (n % b) + y.val
  0 < m ∧ commaMsd b m = y.val

Uses 1 · Used by 7

Statement usesMost significant digit

Used byRecovering the parent of a comma-child · Every number at least the square of the base is a comma-child · The comma-child graph has an infinite path · There is a unique infinite comma-child path from 1 in base 3 · Comma successor · Comma-terminal numbers · Numbers with two comma-children

DefinitionComma successor#✓fully proved

Let \(b\), \(n\) and \(m\) be natural numbers. Then \(m\) is the comma successor of \(n\) in base \(b\) if there is a comma candidate digit \(y < b\) for \(n\) in base \(b\) such that \(m = n + b\,(n \bmod b) + y\) and no digit \(y' < y\) is a comma candidate for \(n\) in base \(b\).

Taking the least candidate \(y\) makes \(m\) the smallest possible next term.

public def IsCommaSucc (b n m : Nat) : Prop :=
  ∃ y : Fin b, IsCommaCandidate b n y ∧ m = n + b * (n % b) + y.val ∧
    ∀ y' : Fin b, y'.val < y.val → ¬ IsCommaCandidate b n y'

Uses 1 · Used by 2

Statement usesComma candidate digits

Used byInfinite comma sequences · Numbers that are not comma successors

DefinitionComma-terminal numbers#✓fully proved

Let \(b\) and \(n\) be natural numbers. Then \(n\) is comma-terminal in base \(b\) if no digit \(y\) with \(0 \le y < b\) is a comma candidate for \(n\) in base \(b\), so \(n\) has no comma successor in base \(b\).

public def IsCommaTerminal (b n : Nat) : Prop :=
  ∀ y : Fin b, ¬ IsCommaCandidate b n y

Uses 1 · Used by 1

Statement usesComma candidate digits

Used byLandmines of the comma sequence

DefinitionInfinite comma sequences#✓fully proved

Let \(b\) and \(v\) be natural numbers and let \(a : \mathbb{N} \to \mathbb{N}\) be a sequence. Then \(a\) is an infinite comma sequence in base \(b\) starting at \(v\) if \(b \ge 2\), \(v > 0\), \(a_1 = v\), and for every \(n \ge 1\) the term \(a_{n+1}\) is the comma successor of \(a_n\) in base \(b\).

Indexing starts at \(1\); the value \(a_0\) is unconstrained.

public def IsInfiniteCommaSeq (b v : Nat) (a : Nat → Nat) : Prop :=
  2 ≤ b ∧ 0 < v ∧ a 1 = v ∧ ∀ n, 1 ≤ n → IsCommaSucc b (a n) (a (n + 1))

Uses 1 · Used by 1

Statement usesComma successor

Used byTerminating comma sequences

DefinitionTerminating comma sequences#✓fully proved

Let \(b\) and \(v\) be natural numbers. The comma sequence in base \(b\) starting at \(v\) terminates if \(b \ge 2\), \(v > 0\), and there is no infinite comma sequence in base \(b\) starting at \(v\).

public def IsCommaTerminating (b v : Nat) : Prop :=
  2 ≤ b ∧ 0 < v ∧ ¬ ∃ a : Nat → Nat, IsInfiniteCommaSeq b v a

Uses 1 · Used by 1

Statement usesInfinite comma sequences

Used byComma sequences terminate in bases 3 to 633

TheoremComma sequences terminate in bases 3 to 633#●ready to prove

For every base \(b\) with \(3 \le b \le 633\) and every positive integer \(v\), the comma sequence in base \(b\) starting at \(v\) terminates, that is, there is no infinite comma sequence in base \(b\) starting at \(v\).

public theorem_wanted commaSequence_terminates_of_base_le_633
    (b v : ℕ) (hb1 : 3 ≤ b) (hb2 : b ≤ 633) (hv : 0 < v) :
    IsCommaTerminating b v

Sources

• Dougherty, Comma Sequences, JIS 28, lines 134–137.

Uses 1

Statement usesTerminating comma sequences

TheoremLandmines of the comma sequence#●ready to prove

Let \(b \ge 2\) and let \(n\) be a positive integer. Then no digit \(y < b\) is a comma candidate for \(n\) in base \(b\) (so \(n\) has no comma successor) if and only if the base-\(b\) representation of \(n\), most significant digit first, is \((b-1) \cdots (b-1)\, x\, (b-1-x)\) with some number \(i \ge 0\) of leading digits \(b - 1\) and \(1 \le x \le b - 2\).

public theorem_wanted isCommaTerminal_iff_digits (b n : ℕ) (hb : 2 ≤ b) (hn : 0 < n) :
    IsCommaTerminal b n ↔ ∃ i x : ℕ, 1 ≤ x ∧ x ≤ b - 2 ∧
      Nat.digits b n = [b - 1 - x, x] ++ List.replicate i (b - 1)

Sources

• Éric Angelini, Michael S. Branicky, Giovanni Resta, N. J. A. Sloane, and David W. Wilson, The Comma Sequence: A Simple Sequence with Bizarre Properties, The Fibonacci Quarterly 62 (2024), no. 3, Theorem 5.1.

Uses 1

Statement usesComma-terminal numbers

TheoremNumbers with two comma-children#●ready to prove

Fix a base \(b \ge 2\), and say that \(n\) has at least two comma-children if there are distinct digits \(y_1 \ne y_2\) below \(b\) that are both comma candidates for \(n\) in base \(b\) (distinct candidates \(y\) give distinct children \(n + b\,(n \bmod b) + y\)). Then a positive integer \(n < b^2\) has at least two comma-children if and only if \(n = (b - 1 - 2x)\, b + x\) for some \(x\) with \(1 \le x\) and \(2x \le b - 1\); and an integer \(n \ge b^2\) has at least two comma-children if and only if its base-\(b\) representation, most significant digit first, is \(d\,(b-1) \cdots (b-1)\, d\,(b-1-d)\) with some number \(i \ge 0\) of middle digits \(b - 1\) and \(1 \le d \le b - 2\).

public theorem_wanted two_commaChildren_iff (b : ℕ) (hb : 2 ≤ b) :
    (∀ n : ℕ, 0 < n → n < b ^ 2 →
      ((∃ y₁ y₂ : Fin b, y₁ ≠ y₂ ∧ IsCommaCandidate b n y₁ ∧ IsCommaCandidate b n y₂) ↔
        ∃ x : ℕ, 1 ≤ x ∧ 2 * x ≤ b - 1 ∧ n = (b - 1 - 2 * x) * b + x)) ∧
    ∀ n : ℕ, b ^ 2 ≤ n →
      ((∃ y₁ y₂ : Fin b, y₁ ≠ y₂ ∧ IsCommaCandidate b n y₁ ∧ IsCommaCandidate b n y₂) ↔
        ∃ d i : ℕ, 1 ≤ d ∧ d ≤ b - 2 ∧
          Nat.digits b n = [b - 1 - d, d] ++ List.replicate i (b - 1) ++ [d])

Sources

• Éric Angelini, Michael S. Branicky, Giovanni Resta, N. J. A. Sloane, and David W. Wilson, The Comma Sequence: A Simple Sequence with Bizarre Properties, The Fibonacci Quarterly 62 (2024), no. 3, Theorem 5.2.

Uses 1

Statement usesComma candidate digits

TheoremRecovering the parent of a comma-child#●ready to prove

Fix a base \(b \ge 2\) and a natural number \(n\). Call \(n\) a comma-child of \(k\) if \(n = k + b\,(k \bmod b) + y\) for some comma candidate digit \(y\) of \(k\) in base \(b\). Let \(f\) be the most significant base-\(b\) digit of \(n\) and let \(x = (n - f) \bmod b\). If \(n\) is a comma-child of a positive integer \(k\), then \(k = n - x b - f\); and if the integer \(n - x b - f\) is negative, then \(n\) is not a comma-child of any positive integer.

public theorem_wanted commaChild_parent_eq (b n : ℕ) (hb : 2 ≤ b) :
    (∀ k : ℕ, 0 < k → (∃ y : Fin b, IsCommaCandidate b k y ∧ n = k + b * (k % b) + y.val) →
      (k : ℤ) = n - ((n - commaMsd b n) % b : ℕ) * b - commaMsd b n) ∧
    ((n : ℤ) - ((n - commaMsd b n) % b : ℕ) * b - commaMsd b n < 0 →
      ¬ ∃ k : ℕ, 0 < k ∧ ∃ y : Fin b, IsCommaCandidate b k y ∧ n = k + b * (k % b) + y.val)

Sources

• Éric Angelini, Michael S. Branicky, Giovanni Resta, N. J. A. Sloane, and David W. Wilson, The Comma Sequence: A Simple Sequence with Bizarre Properties, The Fibonacci Quarterly 62 (2024), no. 3, Lemma 5.3.

Uses 2

Statement usesComma candidate digits · Most significant digit

TheoremNumbers that are not comma successors#●ready to prove

Let \(b \ge 3\) and \(n \ge b^2 - 1\). Then \(n\) is not the comma successor in base \(b\) of any positive integer if and only if \(n = c\, b^i\) for some \(i \ge 2\) and some \(c\) with \(2 \le c \le b - 1\).

public theorem_wanted not_commaSucc_iff (b n : ℕ) (hb : 3 ≤ b) (hn : b ^ 2 - 1 ≤ n) :
    (¬ ∃ k : ℕ, 0 < k ∧ IsCommaSucc b k n) ↔
      ∃ c i : ℕ, 2 ≤ i ∧ 2 ≤ c ∧ c ≤ b - 1 ∧ n = c * b ^ i

Sources

• Éric Angelini, Michael S. Branicky, Giovanni Resta, N. J. A. Sloane, and David W. Wilson, The Comma Sequence: A Simple Sequence with Bizarre Properties, The Fibonacci Quarterly 62 (2024), no. 3, Theorem 5.4.

Uses 1

Statement usesComma successor

TheoremEvery number at least the square of the base is a comma-child#●ready to prove

Let \(b \ge 2\) and \(n \ge b^2\). Then there are a positive integer \(k\) and a comma candidate digit \(y\) of \(k\) in base \(b\) with \(n = k + b\,(k \bmod b) + y\), that is, \(n\) is a comma-child of \(k\).

public theorem_wanted exists_commaParent_of_sq_le (b n : ℕ) (hb : 2 ≤ b) (hn : b ^ 2 ≤ n) :
    ∃ k : ℕ, 0 < k ∧ ∃ y : Fin b, IsCommaCandidate b k y ∧ n = k + b * (k % b) + y.val

Sources

• Éric Angelini, Michael S. Branicky, Giovanni Resta, N. J. A. Sloane, and David W. Wilson, The Comma Sequence: A Simple Sequence with Bizarre Properties, The Fibonacci Quarterly 62 (2024), no. 3, Theorem 5.5.

Uses 1

Statement usesComma candidate digits

TheoremThe comma-child graph has an infinite path#●ready to prove

For every base \(b \ge 2\) there is a sequence \(a_0, a_1, \dots\) of positive integers such that for every \(i\) there is a comma candidate digit \(y\) of \(a_i\) in base \(b\) with \(a_{i+1} = a_i + b\,(a_i \bmod b) + y\), that is, each \(a_{i+1}\) is a comma-child of \(a_i\).

public theorem_wanted exists_infinite_commaChild_path (b : ℕ) (hb : 2 ≤ b) :
    ∃ a : ℕ → ℕ, (∀ i, 0 < a i) ∧
      ∀ i, ∃ y : Fin b, IsCommaCandidate b (a i) y ∧ a (i + 1) = a i + b * (a i % b) + y.val

Sources

• Éric Angelini, Michael S. Branicky, Giovanni Resta, N. J. A. Sloane, and David W. Wilson, The Comma Sequence: A Simple Sequence with Bizarre Properties, The Fibonacci Quarterly 62 (2024), no. 3, Theorem 5.6.

Uses 1

Statement usesComma candidate digits

TheoremThere is a unique infinite comma-child path from 1 in base 3#●ready to prove

There is exactly one sequence \(a_0, a_1, \dots\) of natural numbers with \(a_0 = 1\) such that for every \(i\) there is a comma candidate digit \(y\) of \(a_i\) in base \(3\) with \(a_{i+1} = a_i + 3\,(a_i \bmod 3) + y\), that is, each \(a_{i+1}\) is a base-3 comma-child of \(a_i\).

The paper also describes this path (at branch points it alternately takes the lower and the higher child); that description is not part of this statement.

public theorem_wanted existsUnique_commaChild_path_base_three :
    ∃! a : ℕ → ℕ, a 0 = 1 ∧
      ∀ i, ∃ y : Fin 3, IsCommaCandidate 3 (a i) y ∧ a (i + 1) = a i + 3 * (a i % 3) + y.val

Sources

• Éric Angelini, Michael S. Branicky, Giovanni Resta, N. J. A. Sloane, and David W. Wilson, The Comma Sequence: A Simple Sequence with Bizarre Properties, The Fibonacci Quarterly 62 (2024), no. 3, Theorem 10.1.

Uses 1

Statement usesComma candidate digits

6 fully proved8 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.