Rigorously prove while loop executes $\lceil \log_{2}(\log_{2}(n)) \rceil$ times

Question

Problem

Suppose we have the following code

k := 2
while k < n do
    k := k * k
end while

How many times will the loop execute?

Current Work

My intuitive understanding of the question is "How many times must 2 be squared so that it is greater than or equal to n?". To answer this question, we can solve $2^{2^{m}} = n$ for $m$.

\begin{align} 2^{2^{m}} &= n \\ \log_{2}(2^{2^{m}}) &= \log_{2}(n) \\ 2^{m} &= \log_{2}(n) \\ \log_{2}(2^{m}) &= \log_{2}(\log_{2}(n)) \\ m &= \log_{2}(\log_{2}(n)). \end{align}

Since we are only dealing with natural numbers for the loop iterations, we take the ceiling, $\lceil m \rceil = \lceil \log_{2}(\log_{2}(n)) \rceil$.

This is as far as I've gotten. Although I think my intuition is correct, I am not satisfied with presenting this as an answer. My problem is that I can't seem to figure out how to start writing a formal proof for this that doesn't rely on my intuitive insight.

Answer 1

By induction, we prove that $k = 2^{2^j}$ after $j$ iterations of the loop. Importantly, $2^{2^j}$ is strictly increasing as a function of $j$.

Now, define $m = \log_2(\log_2(n))$. Then, if $j < m$, the loop will not terminate at the conclusion of the $j$th iteration, since $2^{2^j} < 2^{2^m} = n$. Therefore the loop will run at least $m$ times. But the number of iterations is an integer, and $\lceil m \rceil$ is by definition the smallest integer that is at least $m$. So there are at least $\lceil m \rceil$ iterations. To see that it will terminate after the $\lceil m \rceil$th iteration, observe that since $m \le \lceil m \rceil$, we obtain $n = 2^{2^m} \le 2^{2^{\lceil m \rceil}}$. So after $\lceil m \rceil$ steps, $k \ge n$ and the loop will stop executing.