/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilFactor bounds for Fermat numbers
$a(n)$ is the minimum integer $k$ such that the smallest prime factor of the $n$-th Fermat number exceeds $2^{2^n - k}$.
References:
namespace OeisA358684open NatA358684: $a(n)$ is the minimum integer $k$ such that the smallest prime factor of the $n$-th Fermat number exceeds $2^{2^n - k}$. Let $F_n = 2^{2^n} + 1$ be the $n$-th Fermat number, and $P_n$ be its smallest prime factor. The definition of $a(n)$ is equivalent to the closed form: $$a(n) = 2^n - \lfloor \log_2(P_n) \rfloor$$ where $P_n = \operatorname{minFac}(\operatorname{fermatNumber} n)$. The subtraction is defined in $\mathbb{N}$ and is safe since $P_n \le F_n$, implying $\log_2 P_n < 2^n$.
def a (n : ℕ) : ℕ :=
letI pn := minFac (fermatNumber n)
(2 ^ n) - (log2 pn)
The "original" definition: $a'(n)$ is the minimum $k$ such that $P_n > 2^{2^n - k}$.
We use Nat.find which returns the smallest natural number satisfying a predicate.
noncomputable def a' (n : ℕ) : ℕ :=
letI Pn := minFac (fermatNumber n)
Nat.find (show ∃ k, Pn > 2 ^ (2 ^ n - k) from n:ℕPn:ℕ := n.fermatNumber.minFac⊢ ∃ k, Pn > 2 ^ (2 ^ n - k)
n:ℕPn:ℕ := n.fermatNumber.minFac⊢ Pn > 2 ^ (2 ^ n - 2 ^ n)
n:ℕPn:ℕ := n.fermatNumber.minFac⊢ Pn > 1
n:ℕPn:ℕ := n.fermatNumber.minFac⊢ 1 < n.fermatNumber.minFac
n:ℕPn:ℕ := n.fermatNumber.minFac⊢ 1 < (2 ^ 2 ^ n + 1).minFac
exact (Nat.minFac_prime (n:ℕPn:ℕ := n.fermatNumber.minFac⊢ 2 ^ 2 ^ n + 1 ≠ 1 All goals completed! 🐙)).one_lt
)The log2 of the smallest prime factor of $F_n$ is at most $2^n$.
n:ℕ⊢ 2 ^ 2 ^ n + 1 < 2 ^ 2 ^ n + 2 ^ 2 ^ n
n:ℕ⊢ 1 < 2 ^ 2 ^ n
exact one_lt_pow (n:ℕ⊢ 2 ^ n ≠ 0 All goals completed! 🐙) (n:ℕ⊢ 1 < 2 All goals completed! 🐙)The minimization definition is equivalent to the closed form.
n:ℕPn:ℕ := n.fermatNumber.minFacm:ℕhm:log 2 n.fermatNumber.minFac + m < 2 ^ n⊢ n.fermatNumber.minFac ≤ 2 ^ (2 ^ n - m)
refine (lt_pow_succ_log_self (b:=2) (n:ℕPn:ℕ := n.fermatNumber.minFacm:ℕhm:log 2 n.fermatNumber.minFac + m < 2 ^ n⊢ 1 < 2 All goals completed! 🐙) _).le.trans ?_
apply Nat.pow_le_pow_right (n:ℕPn:ℕ := n.fermatNumber.minFacm:ℕhm:log 2 n.fermatNumber.minFac + m < 2 ^ n⊢ 2 > 0 All goals completed! 🐙)
n:ℕPn:ℕ := n.fermatNumber.minFacm:ℕhm:log 2 n.fermatNumber.minFac + m < 2 ^ n⊢ (log 2 n.fermatNumber.minFac).succ + m ≤ 2 ^ n
n:ℕPn:ℕ := n.fermatNumber.minFacm:ℕhm:log 2 n.fermatNumber.minFac + m < 2 ^ nthis:(log 2 n.fermatNumber.minFac + m).succ ≤ 2 ^ n⊢ (log 2 n.fermatNumber.minFac).succ + m ≤ 2 ^ n
All goals completed! 🐙@[category test, AMS 11]
theorem a_0 : a 0 = 0 := ⊢ a 0 = 0 ⊢ 1 - log2 3 = 0; All goals completed! 🐙@[category test, AMS 11]
theorem a_1 : a 1 = 0 := ⊢ a 1 = 0 ⊢ 2 - log2 5 = 0; All goals completed! 🐙@[category test, AMS 11]
theorem a_2 : a 2 = 0 := ⊢ a 2 = 0 ⊢ 4 - log2 17 = 0; All goals completed! 🐙@[category test, AMS 11]
theorem a_3 : a 3 = 0 := ⊢ a 3 = 0
All goals completed! 🐙@[category test, AMS 11]
theorem a_4 : a 4 = 0 := ⊢ a 4 = 0
All goals completed! 🐙@[category test, AMS 11]
theorem a_5 : a 5 = 23 := ⊢ a 5 = 23
All goals completed! 🐙@[category test, AMS 11]
theorem a_6 : a 6 = 46 := ⊢ a 6 = 46
All goals completed! 🐙@[category test, AMS 11]
theorem a_7 : a 7 = 73 := ⊢ a 7 = 73
All goals completed! 🐙Conjecture: the dyadic valuation of A93179(n) - 1 does not exceed 2^n - a(n).
A93179(n) is minFac(fermatNumber n), the smallest prime factor of the n-th Fermat number. The conjecture states that if $P_n$ is the smallest prime factor of the $n$-th Fermat number, then $\nu_2(P_n - 1) \le 2^n - a(n)$. Substituting the definition of $a(n)$, this is equivalent to $\nu_2(P_n - 1) \le \lfloor \log_2(P_n) \rfloor$.
This is Conjecture 3.4 in [SA22].
n:ℕthis:2 ^ 2 ^ n + 1 < 2 ^ (2 ^ n + 1)⊢ log 2 (2 ^ 2 ^ n + 1).minFac ≤ 2 ^ n
n:ℕthis:2 ^ 2 ^ n + 1 < 2 ^ (2 ^ n + 1)⊢ (2 ^ 2 ^ n + 1).minFac ≠ 0n:ℕthis:2 ^ 2 ^ n + 1 < 2 ^ (2 ^ n + 1)⊢ (2 ^ 2 ^ n + 1).minFac < 2 ^ (2 ^ n).succ
n:ℕthis:2 ^ 2 ^ n + 1 < 2 ^ (2 ^ n + 1)⊢ (2 ^ 2 ^ n + 1).minFac ≠ 0 All goals completed! 🐙
n:ℕthis:2 ^ 2 ^ n + 1 < 2 ^ (2 ^ n + 1)⊢ (2 ^ 2 ^ n + 1).minFac < 2 ^ (2 ^ n).succ exact (Nat.minFac_le (n:ℕthis:2 ^ 2 ^ n + 1 < 2 ^ (2 ^ n + 1)⊢ 0 < 2 ^ 2 ^ n + 1 All goals completed! 🐙)).trans_lt thisend OeisA358684