Repdigits, palindromes and reverse multiples

Repdigits, palindromes, reverse multiples and Young graphs, permutiples, digit reversal, special squares by digits.

DefinitionDigit reversal#✓fully proved

For natural numbers \(b\) and \(n\) with \(b \ge 2\), write \(n = \sum_{i\lt k} d_i b^i\) with digits \(0 \le d_i < b\) and leading digit \(d_{k-1} \ne 0\) (so \(k = 0\) when \(n = 0\)). The base-\(b\) reversal of \(n\) is the natural number \(\sum_{i\lt k} d_{k-1-i} b^i\). For the bases \(b = 0\) and \(b = 1\) the reversal of \(n\) is \(n\) itself.

Trailing zeros of \(n\) become leading zeros and are lost: in base \(10\) the reversal of \(120\) is \(21\).

def reverseDigits (b n : ℕ) : ℕ :=
  Nat.ofDigits b (Nat.digits b n).reverse

Used by 11

Used byBasic reverse divisors · In base \(B\), divisors of \(B^2 - 1\) divide reversals of their multiples · Sufficient conditions for a multiple with divisible reversal · Property \(P^*\) · Unfolding property \(P^*\) · Infinitely many multiples with divisible reversal · Reverse divisor · Characterization of reverse divisors · Reverse divisors with quotient \(4\) lack property \(P^*\) · Palindromes with property \(P^*\) · Reverse divisors have quotient \(4\) or \(9\)

TheoremPerfect powers with all decimal digits equal but one (Kihel–Luca)#●ready to prove

Fix a natural number \(l \ge 3\). There are only finitely many perfect \(l\)-th powers \(y = x^l\) (\(x \in \mathbb{N}\)) whose decimal digits are all equal but one, that is, some digit \(c\) occurs in the decimal representation of \(y\) and exactly one digit position of \(y\) holds a digit other than \(c\), apart from the powers \(10^{ln}\) (\(n \in \mathbb{N}\)) and, when \(l = 3\), the cubes \(8 \cdot 10^{3n}\) (\(n \in \mathbb{N}\)).

public theorem_wanted finite_near_repdigit_perfect_powers (l : ℕ) (hl : 3 ≤ l) :
  Set.Finite
    { y : ℕ | (∃ x : ℕ, y = x ^ l) ∧
    (∃ c : ℕ, c < 10 ∧ c ∈ Nat.digits 10 y ∧
    (List.filter (fun a => a != c) (Nat.digits 10 y)).length = 1) ∧ ¬
    ((∃ n : ℕ, y = 10 ^ (l * n)) ∨ (l = 3 ∧ ∃ n : ℕ, y = 8 * 10 ^ (3 * n))) }

Sources

Omar Kihel and Florian Luca, "Perfect Powers with All Equal Digits but One," Journal of Integer Sequences 8 (2005), Article 05.5.7, Theorem 1, lines 134–140, https://cs.uwaterloo.ca/journals/JIS/VOL8/Kihel/kihel7.tex.

TheoremSquares with two blocks of repeated digits#●ready to prove

Let \(n\) be a perfect square whose decimal representation, read from the most significant digit, consists of \(r \ge 1\) copies of a digit \(a\) with \(1 \le a \le 9\) followed by \(s \ge 1\) copies of a digit \(b\) with \(0 \le b \le 9\). Then \(n\) is one of \(16\), \(25\), \(36\), \(49\), \(64\), \(81\), \(144\), \(225\), \(441\), \(1444\) and \(7744\), or there is a natural number \(i\) such that \(n = 10^{2i}\), \(n = 4 \cdot 10^{2i}\) or \(n = 9 \cdot 10^{2i}\).

public theorem_wanted squares_aaabb_classification
    (n : ℕ) (hn : IsSquare n)
    (h : ∃ a b r s : ℕ, 1 ≤ a ∧ a ≤ 9 ∧ b ≤ 9 ∧ 1 ≤ r ∧ 1 ≤ s ∧
      Nat.digits 10 n = List.replicate s b ++ List.replicate r a) :
    n = 16 ∨ n = 25 ∨ n = 36 ∨ n = 49 ∨ n = 64 ∨ n = 81 ∨ n = 144 ∨
    n = 225 ∨ n = 441 ∨ n = 1444 ∨ n = 7744 ∨
    (∃ i, n = 10 ^ (2 * i)) ∨ (∃ i, n = 4 * 10 ^ (2 * i)) ∨
    (∃ i, n = 9 * 10 ^ (2 * i))

Sources

Omar Kihel and Florian Luca, "Perfect Powers With All Equal Digits But One," Journal of Integer Sequences 8 (2005), Article 05.5.7, Theorem, lines 273–279, https://cs.uwaterloo.ca/journals/JIS/VOL8/Kihel/kihel7.tex

TheoremTriangular repdigits#●ready to prove

The positive triangular numbers \(n(n+1)/2\) with \(n \ge 1\) whose decimal representation consists of a single repeated digit are exactly \(1\), \(3\), \(6\), \(55\), \(66\) and \(666\).

theorem_wanted triangular_numbers_single_repeated_digit :
    {m : ℕ |
      (∃ n : ℕ, 1 ≤ n ∧ 2 * m = n * (n + 1)) ∧
        ∃ d : ℕ, d < 10 ∧ d ∈ Nat.digits 10 m ∧
          ∀ a ∈ Nat.digits 10 m, a = d} =
      {1, 3, 6, 55, 66, 666}

Sources

Christian Hercher and Karl Fegert, "Triangular Numbers With a Single Repeated Digit", Theorem 1.

1 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.