\section{The computations for Theorems~\ref{thm:B1upper} and~\ref{thm:B2upper}}\label{app:computations}

All enclosures below are computed in ball arithmetic~\cite{Johansson2017} from exact rational inputs.

\subsection*{Theorem~\ref{thm:B1upper}}
There are two ranges $[s_-,s_+]$ of $s=|a|$: $[0.845,0.849]$ with $\rho=827/1000$, and $[0.849,0.84904]$ with $\rho=8271/10000$. For
each, the rectangle $[s_-,s_+]\times[0,355/113]$ of pairs $(s,\theta)$, where $355/113>\pi$, is covered by boxes, and on each box we certify
\[
  \bigl|\operatorname{Log}\bigl(-\sigma_s(\rho e^{i\theta})\bigr)\bigr|^2-L(\rho)^2>0\qquad\text{for all $(s,\theta)$ in the box},
\]
by a ball enclosure of the left side at $200$ bits. This is the hypothesis of Lemma~\ref{lem:circlehomotopy} for every $s$ in the
range: the range $\theta\in[0,\pi]$ suffices because $\sigma_s(\bar w)=\overline{\sigma_s(w)}$. The enclosure of $|\operatorname{Arg}\xi|$ uses
\[
  |\operatorname{Arg}\xi|=\begin{cases}\arctan(|\operatorname{Im}\xi|/\operatorname{Re}\xi)&\text{if }\operatorname{Re}\xi>0,\\
  \pi-\arctan(|\operatorname{Im}\xi|/|\operatorname{Re}\xi|)&\text{if }\operatorname{Re}\xi<0,\\
  \arccos(\operatorname{Re}\xi/|\xi|)&\text{otherwise},\end{cases}
\]
so that no branch cut is crossed. Adaptive bisection
needs $96282$ boxes for $[0.845,0.849]$ and $476313$ boxes for $[0.849,0.84904]$. The margin is small: at $s=0.849$, $\rho=0.827$ the
minimum of $|\operatorname{Log}(-\sigma_s)|-L(\rho)$ on the circle is about $1.9\cdot10^{-4}$, and at $s=0.84905$, $\rho=0.8271$, $\theta=0.2848$ the
enclosure of $|\operatorname{Log}(-\sigma_s)|^2-L(\rho)^2$ is negative.

\subsection*{Theorem~\ref{thm:B2upper}}
Here all enclosures are computed at $128$ bits.

\emph{The boxes.} The cover of the parameter set $X_{61}$ of the proof has $28853$ boxes, obtained by halving the widest side, starting
from the $8\times16\times8$ grid of $[0,1]\times[-1,1]\times[0,1]$; a box is discarded only if an exact test shows that it misses
$X_{61}$. Each centre is of the form $w_C=(k+li)/40$ and each radius of the form $\rho=k'/1000$; $25454$ boxes use $w_C=0$.

\emph{Condition (i)} is checked in exact rational arithmetic over the whole box: the exact range of $|a-w_C|^2$ over the segment of values
of $a_1$ and over the rectangle of values of $a_2$ is compared with $(\rho\pm1/200)^2$.

\emph{Condition (ii).} Write $p=(r_1,x_2,y_2)$, $p_0$ for the centre of the box, $\hat t_k$ for its half-widths, $t=p-p_0$ (so
$|t_k|\le {\hat t}_k$) and $\partial_k=\partial/\partial p_k$. The interval $\theta\in[0,710/113]\supset[0,2\pi]$ is covered adaptively by
pieces $I$, with midpoint $\theta_I$ and half-width $\eta$. On each piece we certify
\[
  \bigl|\operatorname{Log}\bigl(-\sigma(p,w)\bigr)\bigr|-L(r_I)>0\qquad\text{for every $p$ in the box and every }w=w_C+\rho e^{i\theta},\ \theta\in I,
\]
where $r_I$ is an upper bound of $|w|$ on the piece; since $L$ is increasing, this gives (ii) on the piece. The left side is bounded
below by the first of the following five certified bounds that is positive.
\begin{enumerate}
\item[(a)] The ball enclosure of $|\operatorname{Log}(-\sigma)|^2-L(r_I)^2$ over the box and the piece, computed as for Theorem~\ref{thm:B1upper},
  with $|\operatorname{Log}\xi|\ge|\log|\xi||$ used instead where $|\xi|<e^{-L}$ or $|\xi|>e^{L}$ (this is needed where $\sigma$ has a zero on the circle).
\item[(b)] The same, applied to an enclosure of $\sigma$ from the mean value theorem: for fixed $w$,
  \[
    \sigma(p,w)-\sigma(p_0,w)=\sum_kt_k\int_0^1\partial_k\sigma(p_0+st,w)\,ds\ \in\ \sum_k[-\hat t_k,\hat t_k]\,E_k,
  \]
  where $E_k$ is the enclosure of $\partial_k\sigma$ over the box; each integral lies in $E_k$, since an enclosure is a rectangle and
  hence convex.
\item[(c)] The same with $\theta$ moving as well, from $\theta_I$: this adds $[-\eta,\eta]$ times an enclosure of
  $\partial\sigma/\partial\theta=i(w-w_C)\,\partial\sigma/\partial w$.
\item[(d)] Where $\inf|\sigma|>0$ is certified on the box: let $\phi_0$ be a logarithm of $-\sigma(p_0,w)$ and $\phi$ the continuous
  logarithm of $-\sigma(\cdot,w)$ along the segment from $p_0$ to $p$ with $\phi(p_0)=\phi_0$. Then
  \[
    \phi(p)=\phi_0+\sum_kt_kg_k+\epsilon,\qquad g_k=\frac{\partial_k\sigma}{\sigma}(p_0,w),\qquad
    |\epsilon|\le\frac12\sum_{k,l}{\hat t}_k\hat t_l\sup\bigl|\partial_k\partial_l\phi\bigr|,
  \]
  where $\partial_k\partial_l\phi=\partial_k\partial_l\sigma/\sigma-\partial_k\sigma\,\partial_l\sigma/\sigma^2$. Since
  $|\operatorname{Log}(-\sigma(p,w))|=\min_{n\in\mathbb Z}|\phi(p)-2\pi in|$, it is at least the least of the bounds
  \[
    |\phi(p)-2\pi in|\ \ge\ \operatorname{Re}\bigl(\bar u(\phi_0-2\pi in)\bigr)-\sum_k\hat t_k\bigl|\operatorname{Re}(\bar ug_k)\bigr|-|\epsilon|
  \]
  for the three $n$ nearest to $\operatorname{Im}\phi_0/2\pi$, with a unit $u$ close to the direction of $\phi_0-2\pi in$, and
  \[
    |\phi(p)-2\pi in|\ \ge\ 4\pi-|\operatorname{Im}\phi_0-2\pi n^*|-|\phi(p)-\phi_0|,\qquad
    |\phi(p)-\phi_0|\le\sum_k\hat t_k|g_k|+|\epsilon|,
  \]
  for the other $n$, where $n^*$ is the middle one of the three.
\item[(e)] Where $\inf|\sigma|>0$ is certified on the box:
  \[
    \bigl|\operatorname{Log}\bigl(-\sigma(p,w)\bigr)\bigr|\ \ge\ \bigl|\operatorname{Log}\bigl(-\sigma(p_0,w)\bigr)\bigr|-\sum_k\hat t_k\,\frac{\sup|\partial_k\sigma|}{\inf|\sigma|};
  \]
  along a segment in the box, with $w$ fixed, a continuous logarithm of $-\sigma$ moves by at most this sum, and
  $|\operatorname{Log}\xi|=\min_{n\in\mathbb Z}|\log \xi+2\pi in|$ is $1$-Lipschitz in that logarithm.
\end{enumerate}
The partial derivatives are exact: each term of $\sigma$ is $w/(w-a)+\bar aw/(1-\bar aw)$, with $\partial/\partial a=w/(w-a)^2$,
$\partial/\partial\bar a=w/(1-\bar aw)^2$, $\partial^2/\partial a^2=2w/(w-a)^3$, $\partial^2/\partial\bar a^2=2w^2/(1-\bar aw)^3$ and
$\partial^2/\partial a\,\partial\bar a=0$, and its derivative in $w$ is $-a/(w-a)^2+\bar a/(1-\bar aw)^2$.

\emph{Condition (iii).} The zeros of $\widehat P_0$ at a rational point of the box are isolated by validated root enclosures and compared
with $C$.