Documentation

FormalConjectures.Wikipedia.LychrelNumbers

Lychrel numbers in base 10 #

A (base-10) Lychrel number is a positive integer which never becomes a palindrome under the iteration

$$a_{0} = n, \qquad a_{k+1} = a_k + \operatorname{rev}_{10}(a_k).$$

One commonly stated conjectural direction is that there are no Lychrel numbers in base 10. The smallest widely studied open case is 196.

References:

source
@[reducible, inline]
abbrev LychrelNumbers.base :
ℕ

The base (10) used for digit reversal.

Equations
Instances For
    source
    def LychrelNumbers.rev10 (n : ℕ) :
    ℕ

    The digit-reversal map $\operatorname{rev}_{10}(n)$.

    Implementation note: Nat.digits base n returns the digits of n in little-endian order. Reversing this list and interpreting it again as little-endian digits gives the usual digit reversal.

    Equations
    Instances For
      source
      def LychrelNumbers.IsPalindrome10 (n : ℕ) :
      Prop

      A number is a (base-10) palindrome if it equals its digit reversal.

      Equations
      Instances For
        source
        def LychrelNumbers.lychrelStep (n : ℕ) :
        ℕ

        One step of the Lychrel iteration: n ↦ n + rev10 n.

        Equations
        Instances For
          source
          def LychrelNumbers.IsLychrel10 (n : ℕ) :
          Prop

          The number $n$ is a (base-10) Lychrel number if no iterate of the Lychrel process is a palindrome.

          Equations
          Instances For
            source
            theorem LychrelNumbers.no_lychrel_numbers_base10 :
            True ↔ ∀ (n : ℕ), 0 < n → ¬IsLychrel10 n

            Lychrel conjecture (base 10): conjecturally, there are no Lychrel numbers in base 10.

            Equivalently, every positive integer eventually becomes a palindrome under the Lychrel iteration.

            source
            theorem LychrelNumbers.isLychrel10_196 :
            True ↔ IsLychrel10 196

            The first widely studied open case: whether 196 is a base-10 Lychrel number.

            source
            theorem LychrelNumbers.eventually_palindrome_base10 :
            (∀ (n : ℕ), 0 < n → ∃ (k : ℕ), IsPalindrome10 (lychrelStep^[k] n)) ↔ ∀ (n : ℕ), 0 < n → ¬IsLychrel10 n

            An equivalent formulation of no_lychrel_numbers_base10.

            source
            theorem LychrelNumbers.rev10_120 :
            rev10 120 = 21

            Sanity check: digit reversal of 120 is 21.

            source
            theorem LychrelNumbers.palindrome_121 :
            IsPalindrome10 121

            Sanity check: 121 is a base-10 palindrome.

            source
            theorem LychrelNumbers.lychrelIter_56_one :
            lychrelStep^[1] 56 = 121

            Sanity check: 56 → 121 in one Lychrel step.

            source
            theorem LychrelNumbers.eventually_palindrome_56 :
            ∃ (k : ℕ), IsPalindrome10 (lychrelStep^[k] 56)

            Sanity check: the Lychrel iteration at 56 reaches a palindrome.