$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:

• A358684
• SA22 Lorenzo Sauras-Altuzarra, Some properties of the factors of Fermat numbers, Art Discrete Appl. Math. (2022).

def a (n : ℕ) : ℕ

A358684: $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$.

Equations

• a n = 2 ^ n - n.fermatNumber.minFac.log2

noncomputable def a' (n : ℕ) : ℕ

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.

Equations

• a' n = Nat.find ⋯

theorem a_equiv_a' (n : ℕ) : a n = a' n

The minimization definition is equivalent to the closed form.

theorem zero : a 0 = 0

theorem one : a 1 = 0

theorem two : a 2 = 0

theorem three : a 3 = 0

theorem four : a 0 = 0

theorem five : a 5 = 23

theorem six : a 6 = 46

theorem seven : a 7 = 73

theorem oeis_358684_conjecture_0 (n : ℕ) : padicValNat 2 (n.fermatNumber.minFac - 1) ≤ 2 ^ n - a n

Conjecture: the dyadic valuation of A093179(n) - 1 does not exceed 2^n - a(n).

A093179(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].