FormalConjectures/OEIS/103662.lean

GitHub source file

8 declarations, 2 contain sorry, 0 declared as axioms

1. def OeisA103662.IsValidZerolessPower A helper predicate: $b^n$ is a power with base $>1$ whose decimal representation does not contain the digit 0 line 41 source

   Source documentation

   A helper predicate: $b^n$ is a power with base $>1$ whose decimal representation does not contain the digit 0. We assume $n$ is the exponent, $n \ge 1$.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat

   Proof uses: And, GT.gt, OfNat.ofNat, Not, Membership.mem, List, Nat.digits, HPow.hPow

   7 instances, coercions and auxiliary constants left out.

   def IsValidZerolessPower (n b : ℕ) : Prop :=
   …

2. def OeisA103662.a The primary defining sequence a line 52 source

   Source documentation

   The primary defining sequence a. a n is the smallest power with base $>1$ and exponent $n$ whose decimal representation doesn't contain the digit 0. $$a(n) = (\min \{ b \in \mathbb{N} \mid b > 1, \text{decimal representation of } b^n \text{ contains no digit } 0 \})^n$$ If no such base exists, sInf of an empty set of naturals returns 0, so a n = 0.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat

   Proof uses: InfSet.sInf, Set.ofPred, OeisA103662.IsValidZerolessPower, HPow.hPow

   5 instances, coercions and auxiliary constants left out.

   noncomputable def a (n : ℕ) : ℕ :=
   …

3. theorem OeisA103662.a_0 Term theorems verifying the first few values of the sequence against the official OEIS b-file line 58 source

   Source documentation

   Term theorems verifying the first few values of the sequence against the official OEIS b-file

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Eq, Nat, OeisA103662.a, OfNat.ofNat

   Proof uses: Eq.refl

   2 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem a_0 : a 0 = 1 := by
   …

   Mentions: OeisA103662.a

4. theorem OeisA103662.a_1 line 62 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Eq, Nat, OeisA103662.a, OfNat.ofNat

   Proof uses: Eq.mpr, InfSet.sInf, Set.ofPred, OeisA103662.IsValidZerolessPower, id, congrFun', congrArg, pow_one, And, LT.lt, Not, Membership.mem, List, Nat.digits, Set, funext, GT.gt, HPow.hPow, congr, IsLeast.csInf_eq and 33 more

   33 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

   Open to load the checked before-and-after goal states.

5. theorem OeisA103662.a_2 line 68 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Eq, Nat, OeisA103662.a, OfNat.ofNat

   Proof uses: id, HPow.hPow, InfSet.sInf, Set.ofPred, OeisA103662.IsValidZerolessPower, congr_arg, And, LE.le, Nat.succ, Not, Membership.mem, List, Nat.digits, IsLeast.csInf_eq, And.intro, Set, lowerBounds, And.symm, of_eq_true, Eq.trans and 35 more

   32 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

   Open to load the checked before-and-after goal states.

6. theorem OeisA103662.a_3 line 74 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Eq, Nat, OeisA103662.a, OfNat.ofNat

   Proof uses: id, HPow.hPow, InfSet.sInf, Set.ofPred, OeisA103662.IsValidZerolessPower, Eq.trans, And, GT.gt, Not, Membership.mem, List, Nat.digits, Nat.succ, Eq.mpr, congrArg, IsLeast.csInf_eq, And.intro, Set, lowerBounds, Nat.le.refl and 34 more

   33 instances, coercions and auxiliary constants left out.

   Tactic trace: 8 steps

   Open to load the checked before-and-after goal states.

7. theorem OeisA103662.conjecture For statistical reasons it is conjectured that the sequence is finite sorry line 113 source

   Source documentation

   For statistical reasons it is conjectured that the sequence is finite. Finite means here that for some $n$, no power $b^n$ with base $b > 1$ has a zeroless decimal representation, which in our definition results in $a(n) = 0$.

   This holds for $n = 2500$ (source). Take any integer $b > 1$ and let $N = b^{2500}$. Since $b \ge 2$, we have $N \ge 2^{2500} > 10^5$, so $N$ has at least six decimal digits. We split into four cases depending on the divisibility of $b$ by $2$ and $5$:

   • If $10 \mid b$: Then $10 \mid N$, so the units digit of $N$ is $0$.
   • If $b$ is odd and $5 \nmid b$: Since $b$ is odd and the Carmichael function satisfies $\lambda(16) = 4 \mid 2500$, we have $N \equiv 1 \pmod{16}$. Since $5 \nmid b$ and $\varphi(5^5) = 2500$, Euler's totient theorem gives $N \equiv 1 \pmod{3125}$. By the Chinese Remainder Theorem, $N \equiv 1 \pmod{50000}$ (as $16 \cdot 3125 = 50000$), so the tens digit of $N$ is $0$.
   • If $b$ is odd and $5 \mid b$: As above, $N \equiv 1 \pmod{16}$. Since $5 \mid b$ and $2500 \ge 4$, we also have $5^4 = 625 \mid N$, so $N \equiv 0 \pmod{625}$. Since $16 \cdot 625 = 10^4$ and $625 \equiv 1 \pmod{16}$, the Chinese Remainder Theorem gives $N \equiv 625 \pmod{10^4}$. Because $N > 10^4$, the last four digits of $N$ are $0625$, so its thousands digit is $0$.
   • If $b$ is even and $5 \nmid b$: Since $2 \mid b$ and $2500 \ge 5$, we have $2^5 = 32 \mid N$, so $N \equiv 0 \pmod{32}$. Since $5 \nmid b$, Euler's theorem again gives $N \equiv 1 \pmod{3125}$. Because $32 \cdot 3125 = 10^5$ and $9376 = 293 \cdot 32 = 3 \cdot 3125 + 1$, the Chinese Remainder Theorem gives $N \equiv 9376 \pmod{10^5}$. Since $N > 10^5$, the last five digits of $N$ are $09376$, so its ten-thousands digit is $0$.

   In every case, the decimal representation of $N$ contains the digit $0$, so $a(2500) = 0$.

   L4DEL explanation

   For statistical reasons it is conjectured that the sequence is finite. Finite means here that for some $n$, no power $b^n$ with base $b > 1$ has a zeroless decimal representation, which in our definition results in $a(n) = 0$. This holds for $n = 2500$ (source). Take any integer $b > 1$ and let $N = b^{2500}$. Since $b \ge 2$, we have $N \ge 2^{2500} > 10^5$, so $N$ has at least six decimal digits. We split into four cases depending on the divisibility of $b$ by $2$ and $5$: - If $10 \mid b$: Then $10 \mid N$, so the units digit of $N$ is $0$. - If $b$ is odd and $5 \nmid b$: Since $b$ is odd and the Carmichael function satisfies $\lambda(16) = 4 \mid 2500$, we have $N \equiv 1 \pmod{16}$. Since $5 \nmid b$ and $\varphi(5^5) = 2500$, Euler's totient theorem gives $N \equiv 1 \pmod{3125}$. By the Chinese Remainder Theorem, $N \equiv 1 \pmod{50000}$ (as $16 \cdot 3125 = 50000$), so the tens digit of $N$ is $0$. - If $b$ is odd and $5 \mid b$: As above, $N \equiv 1 \pmod{16}$. Since $5 \mid b$ and $2500 \ge 4$, we also have $5^4 = 625 \mid N$, so $N \equiv 0 \pmod{625}$. Since $16 \cdot 625 = 10^4$ and $625 \equiv 1 \pmod{16}$, the Chinese Remainder Theorem gives $N \equiv 625 \pmod{10^4}$. Because $N > 10^4$, the last four digits of $N$ are $0625$, so its thousands digit is $0$. - If $b$ is even and $5 \nmid b$: Since $2 \mid b$ and $2500 \ge 5$, we have $2^5 = 32 \mid N$, so $N \equiv 0 \pmod{32}$. Since $5 \nmid b$, Euler's theorem again gives $N \equiv 1 \pmod{3125}$. Because $32 \cdot 3125 = 10^5$ and $9376 = 293 \cdot 32 = 3 \cdot 3125 + 1$, the Chinese Remainder Theorem gives $N \equiv 9376 \pmod{10^5}$. Since $N > 10^5$, the last five digits of $N$ are $09376$, so its ten-thousands digit is $0$.

   Sources and attribution: Pinned Lean source (1646ca16afd6)

   depends on sorry what this means

   Statement uses: Exists, Nat, Eq, OeisA103662.a, OfNat.ofNat

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   2 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem conjecture : ∃ n : ℕ, a n = 0 := by
   …

   Mentions: OeisA103662.a

8. theorem OeisA103662.conjecture.variants.a_40 $a(40)$, if it exists, is not known sorry line 123 source

   Source documentation

   $a(40)$, if it exists, is not known.

   This claim is rooted in the finiteness conjecture. The most direct mathematical expression of the open problem concerning $a(40)$ is the negation of the existence of a valid base.

   depends on sorry what this means

   Statement uses: Not, Exists, Nat, OeisA103662.IsValidZerolessPower, OfNat.ofNat

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   2 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem conjecture.variants.a_40 :
     ¬ ∃ (b : ℕ), IsValidZerolessPower 40 b := by
   …

   Mentions: OeisA103662.IsValidZerolessPower