1: \begin{proof}

2: The trivial bound (\ref{lehm}) is tighter than our new bound at $t=5.867\times 10^9$  and remains so for $t$ all the way down to $t=226.7088\ldots$. We checked the range $[2,230]$ rigorously by computer as follows.

3: 

4: We implemented an interval arithmetic version of the Euler--MacLaurin summation formula that, given an interval $\underline{t}$ returns an interval that includes $|\zeta(\frac{1}{2}+it)|$ for all $t\in\underline{t}$. We divided the line segment $[2,230]$ into pieces of length $1/1024$ and for each piece, checked that $|\zeta(\frac{1}{2}+it)|$ did not exceed our bound. Specifically, if we are considering $\underline{t}=[a,a+1/1024]$ and we know that for $t\in\underline{t}$ that $|\zeta(\frac{1}{2}+it)|\in[x,y]$, then we check $y<0.732 a^{\frac{1}{6}} \log a$. No counter examples exist for $t\in[2,230]$ and this establishes the lemma.

5: \end{proof}

6: