\section{The certificate}\label{app:cert}

In this appendix, we use the notation of Section~\ref{sec:digits}. We give the error terms of the ball evaluation of the recursion, on which the code is based, and describe what was computed.

\subsection{The recursion in ball arithmetic}\label{ssec:balls}
For a step path with rational data, the evaluation produces balls containing $\Psi_\kappa(0,\lambda)$, $\partial_x\Psi_\kappa(0,\lambda)$, the values of $Q$ at the level boundaries, and the integrals of $1-Q$ over the levels. Since the recursion is a chain of Gaussian convolutions of analytic integrands, the trapezoid rule on a lattice converges exponentially fast, and analytic continuation into a strip bounds its error. We now give the error terms.

In this subsection, $M$ denotes the number of levels, not of patterns. Fix rationals $0<s_0<\dots<s_M=1$, $0\le c_0\le\dots\le c_{M-1}$ with $c_{M-1}>0$, and $\lambda$, and let $\kappa=c_i$ on $[s_i,s_{i+1})$ and $\kappa=0$ on $[0,s_0)$. We write $b_i^2=s_{i+1}-s_i$, $\tau_i^2=1-s_i$, $\mathsf d_i=\frac12\int_{s_i}^1\kappa$ and $\Psi_i=\Psi_\kappa(s_i,\cdot)$, and we let $\varphi_b$ denote the density of $N(0,b^2)$. Then $\Psi_M=|\cdot|$ and $\Psi_\kappa(0,\lambda)=\E\Psi_0(\lambda+\sqrt{s_0}z)$. By Lemma~\ref{lem:flow}(b), a level may be cut into several with the same $c$ without changing anything, so the grid of $s_i$ can be refined freely.

For $c_i>0$, we put $\dA_i=\exp(c_i\Psi_{i+1})$ and $\dB_i=\exp(c_i\Psi_i)$, so that $\dB_i(x)=\E\dA_i(x+b_iz)$ and $\dA_i=\dB_{i+1}^{\theta_i}$ with $\theta_i=c_i/c_{i+1}\in[0,1]$. The law of $X_{s_{i+1}}$ given $X_{s_i}=x$ is that of $x+W$, where $W$ has density proportional to $\varphi_{b_i}(y)\dA_i(x+y)$, and we write $\E^i_x$ for this tilted law. For $c_i=0$, the tilted law is the Gaussian law, with $\dA_i=1$. Put $\dE_i(x)=\E^i_x\Psi_{i+1}(x+W)$.

\begin{lemma}\label{lem:rec-elementary}
\begin{enumerate}[label=\textup{(\alph*)}]
\item $\Psi_i$ is even, convex and $1$-Lipschitz.
\item $\Psi_i(x)\ge|x|+\mathsf d_i$, and $\psi_i(x):=\Psi_i(x)-|x|-\mathsf d_i$ is nonnegative and nonincreasing on $x\ge0$.
\item $\dB_i\ge\dA_i$.
\item $\Psi_i(x)\le|x|+\bar X_i$, where $\bar X_i:=\sqrt{2\tau_i^2/\pi}+\mathsf d_i$.
\item For $x\ge0$, $1-\Psi_i'(x)\le2\Nc(-x/\tau_i)\le\exp(-x^2/(2\tau_i^2))$. So $1-\Psi_i'(x)^2\le2\exp(-x^2/(2\tau_i^2))$ for all $x$.
\end{enumerate}
\end{lemma}

\begin{proof}
Parts (a), (b), (d) are Lemma~\ref{lem:flow-compare}(i), (iv), with $\Psi_i'\le1$ for the monotonicity in (b). For (c), convexity gives $\Psi_{i+1}(x+y)\ge\Psi_{i+1}(x)+\Psi_{i+1}'(x)y$, and $\E\exp(tz)\ge1$. Part (e) is Lemma~\ref{lem:response-t0}(b), and for the last claim we use that $\Psi_i'$ is odd and $1-\Psi_i'^2\le2(1-|\Psi_i'|)$.
\end{proof}

Let $\dk(\eta)=(\eta+\sqrt{\eta^2+4})/2$, so that $\dk^2=\eta\dk+1$.

\begin{lemma}\label{lem:rec-strip}
Let $f>0$ on $\R$ with $\log f$ being $c$-Lipschitz, let $b>0$, $\mathcal H(x)=\E f(x+bz)$, and let $\E_{\mathrm t}$ be the tilted law at $x$, under which $W$ has density proportional to $\varphi_b(y)f(x+y)$. For $\zeta=x+\mathrm iy$:
\begin{enumerate}[label=\textup{(\roman*)}]
\item $\mathcal H(\zeta)=\exp(y^2/(2b^2))\mathcal H(x)\E_{\mathrm t}\exp(\mathrm iyW/b^2)$, so $|\mathcal H(\zeta)|\le\exp(y^2/(2b^2))\mathcal H(x)$.
\item $\E_{\mathrm t}W^2\le\dk(cb)^2b^2$.
\item $\operatorname{Re}\E_{\mathrm t}\exp(\mathrm iyW/b^2)\ge\varpi(y):=1-y^2\dk(cb)^2/(2b^2)$, which is positive for $|y|<\sqrt2b/\dk(cb)$. On that strip $\log\mathcal H$ is analytic, $|\operatorname{Im}\log(\mathcal H(\zeta)\exp(-y^2/(2b^2))/\mathcal H(x))|<\pi/2$, and $0\le-\log|\E_{\mathrm t}\exp(\mathrm iyW/b^2)|\le-\log\varpi(y)$.
\end{enumerate}
\end{lemma}

\begin{proof}
For (i), we complete the square in $\varphi_b(y'-\zeta)$. For (ii), Gaussian integration by parts gives $\E_{\mathrm t}W^2=b^2+b^2\E_{\mathrm t}[W(\log f)'(x+W)]\le b^2+b^2c\sqrt{\E_{\mathrm t}W^2}$, and we solve the quadratic. Part (iii) follows from $\cos t\ge1-t^2/2$ and (ii).
\end{proof}

We apply this with $f=\dA_{i+1}$, $b=b_{i+1}$, $c=c_{i+1}>0$, since $\log\dA_{i+1}$ is $c_{i+1}$-Lipschitz by Lemma~\ref{lem:rec-elementary}(a), also at the top level. Fix a strip half-width $a_i<\sqrt2b_{i+1}/\dk_{i+1}$, with $\dk_{i+1}=\dk(c_{i+1}b_{i+1})$, and write $\varpi_i=\varpi(a_i)$. For $\zeta=x+\mathrm iy$, $|y|\le a_i$, and $\theta\in[0,1]$, we have
\begin{equation}\label{eq:dig-strip}
\begin{aligned}
  |\dB_{i+1}(\zeta)^\theta|&\le\exp(\theta a_i^2/(2b_{i+1}^2))\dB_{i+1}(x)^\theta,\\
  |\Psi_{i+1}(\zeta)|&\le\Psi_{i+1}(x)+K_i,&K_i&:=\bigl(a_i^2/(2b_{i+1}^2)+\pi/2-\log\varpi_i\bigr)/c_{i+1},\\
  |\Psi_{i+1}'(\zeta)|&\le\bar{\dB}_i,&\bar{\dB}_i&:=(\dk_{i+1}b_{i+1}+a_i)/(c_{i+1}b_{i+1}^2\varpi_i).
\end{aligned}
\end{equation}
The first line is Lemma~\ref{lem:rec-strip}(i), and the second is (iii), with $\Psi_{i+1}>0$ on $\R$. The third follows from $\mathcal H'(\zeta)=\int((y'-\zeta)/b^2)\varphi_b(y'-\zeta)f(y')\dd y'$ and $\E_{\mathrm t}|W|\le\dk_{i+1}b_{i+1}$. Let $H=N/\dB_{i+1}$ with $N(\zeta)=\int\varphi_{b_{i+1}}(y'-\zeta)\dA_{i+1}(y')\phi(y')\dd y'$ and $\phi$ real, $|\phi|\le S$ on $\R$. Then
\begin{equation}\label{eq:dig-strip-H}
  |H(\zeta)|\le S/\varpi_i,\qquad |\dA_i(\zeta)H(\zeta)|\le\exp(\theta_ia_i^2/(2b_{i+1}^2))\dA_i(x)S/\varpi_i.
\end{equation}
If $c_{i+1}=0$, then $\Psi_{i+1}$ is entire, and with $\mathsf f_i:=\exp(a_i^2/(2b_{i+1}^2))$ we have $|\Psi_{i+1}(\zeta)|\le\mathsf f_i\Psi_{i+1}(x)$, $|\Psi'_{i+1}(\zeta)|\le\mathsf f_i$ and $|H(\zeta)|\le\mathsf f_iS$. In that case we put $\varpi_i=1$, $K_i=0$, $\bar{\dB}_i=\mathsf f_i$, and take $a_i<\sqrt2b_{i+1}$.

\begin{lemma}\label{lem:rec-trapezoid}
If $f$ is analytic on $|\operatorname{Im}y|<a'$, $a<a'$, $\int|f(y+\mathrm iy')|\dd y\le\mathsf F$ for $|y'|\le a$, and $f$ decays as $|\operatorname{Re}y|\to\infty$ uniformly in the strip, then
\[
  \Bigl|\mathsf h\sum_jf(j\mathsf h)-\int f\Bigr|\le\frac{2\mathsf F}{\exp(2\pi a/\mathsf h)-1}.
\]
For $J\mathsf h>cb^2$, the terms $t_j:=\mathsf h\varphi_b(j\mathsf h)\exp(cj\mathsf h)$ satisfy $t_{j+1}/t_j\le\mathsf q:=\exp(-J\mathsf h^2/b^2+c\mathsf h)<1$ for $j\ge J$, so $\sum_{|j|>J}t_{|j|}\le2t_J\mathsf q/(1-\mathsf q)=:\dtail(c)$.
\end{lemma}

\begin{proof}
The first bound is Poisson summation with the Fourier transform of $f$ bounded by $\mathsf F\exp(-a|\omega|)$ after moving the contour, and the geometric series over $\omega=2\pi n/\mathsf h$; see \cite[Theorem~5.1]{TW14}. The second is a geometric series.
\end{proof}

The tables use nested lattices: $\mathsf h_i$ is an integer multiple of $\mathsf h_{i+1}$, so no interpolation occurs. The table of $\Psi_i$ holds $x\in\mathsf h_i\mathbb Z$, $0\le x\le Y_i$, with $Y_i\ge Z\tau_i$, $Z=10$. For the quadrature at level $i$, let $\dtail_i(c)$ be $\dtail(c)$ of Lemma~\ref{lem:rec-trapezoid} with $b=b_i$, $\mathsf h=\mathsf h_{i+1}$, $J=J_i$, and put
\[
  E_i:=\frac{2\exp(a_i^2/(2b_i^2))}{\exp(2\pi a_i/\mathsf h_{i+1})-1},\qquad E_i':=E_i\exp\Bigl(\frac{\theta_ia_i^2}{2b_{i+1}^2}\Bigr),\qquad\mathsf r_i:=E_i'+\dtail_i(c_i).
\]
Let $\mathsf T_i,\mathsf N_i,\mathsf S_i$ be the sums $\sum_{|j|\le J_i}\mathsf h_{i+1}\varphi_{b_i}(j\mathsf h_{i+1})\dA_i(y_j)\phi(y_j)$ with $y_j=x+j\mathsf h_{i+1}$, for $\phi=1$, $\Psi_{i+1}'$, $\Psi_{i+1}$ respectively.

\begin{proposition}\label{prop:rec-level}
Let $x\in\mathsf h_i\mathbb Z$.
\begin{enumerate}[label=\textup{(\alph*)}]
\item If $c_i>0$, then $|\mathsf T_i-\dB_i|\le\mathsf r_i\dB_i$, so $c_i\Psi_i(x)$ lies in $\log\mathsf T_i\pm(-\log(1-\mathsf r_i))$. Further
\begin{align*}
  |\mathsf N_i-\dB_i\Psi_i'|&\le(E_i'\bar{\dB}_i+\dtail_i(c_i))\dB_i,\\
  |\mathsf S_i-\dB_i\dE_i|&\le\bigl(E_i'(|x|+\dk_ib_i+\bar X_{i+1}+K_i)+(|x|+\bar X_{i+1}+1)\dtail_i(c_i+1)\bigr)\dB_i.
\end{align*}
A ratio of a sum $\mathsf N$ with error $\mathsf r_{\mathrm n}\dB_i$ to the denominator $\mathsf T_i$ has error at most $(\mathsf r_{\mathrm n}+\mathsf r_i|\mathsf N/\mathsf T_i|)/(1-\mathsf r_i)$.
\item If $c_i=0$, put $\mathsf C=|x|+\bar X_{i+1}$. The trapezoid sums of $\varphi_{b_i}$ times $\Psi_{i+1},\Psi_{i+1}^2,\Psi_{i+1}'$ have errors at most
\[
  E_i\mathsf C_1+(\mathsf C+1)\dtail_i(1),\qquad E_i\mathsf C_2+(\mathsf C+1)^2\dtail_i(2),\qquad E_i\mathsf C_3+\dtail_i(0),
\]
where $(\mathsf C_1,\mathsf C_2,\mathsf C_3)=(\mathsf C+b_i+K_i,(\mathsf C+b_i+K_i)^2,\bar{\dB}_i)$ if $c_{i+1}>0$, and $(\mathsf f_i(\mathsf C+b_i),\mathsf f_i^2(\mathsf C+b_i)^2,\mathsf f_i)$ if $c_{i+1}=0$. The outer integral for $\Psi_\kappa(0,\lambda)$ and $u_0$ is this case with variance $s_0$.
\item At the top level $i=M-1$, with $c=c_{M-1}$, $b=b_{M-1}$, $x\ge0$, $\mathsf p_\pm=\Nc(\pm x/b+cb)$ and $\mathsf Q=\mathrm e^{cx}\mathsf p_++\mathrm e^{-cx}\mathsf p_-$, one has the closed forms
\[
  \Psi_{M-1}=\frac{cb^2}2+\frac{\log\mathsf Q}c,\quad\Psi_{M-1}'=\frac{\mathrm e^{cx}\mathsf p_+-\mathrm e^{-cx}\mathsf p_-}{\mathsf Q},\quad\dE_{M-1}=cb^2+x\Psi_{M-1}'+\frac{2b\Nd(x/b)\mathrm e^{-c^2b^2/2}}{\mathsf Q}.
\]
\item For $|y|>Y_i$, $\Psi_i(y)$ lies in $|y|+\mathsf d_i+[0,\bar\psi_i]$, with $\bar\psi_i$ the upper end of the enclosure of $\psi_i(Y_i)$, and $\Psi_i'(y)$ lies in $\sgn(y)[1-\exp(-Y_i^2/(2\tau_i^2)),1]$.
\end{enumerate}
\end{proposition}

\begin{proof}
(a) Let $\phi=1$. By \eqref{eq:dig-strip} with $\theta=\theta_i$, the function $y\mapsto\varphi_{b_i}(y-x)\dA_i(y)$ has, on $|\operatorname{Im}y|\le a_i$, $L^1$ norm at most $\exp(a_i^2/(2b_i^2)+\theta_ia_i^2/(2b_{i+1}^2))\dB_i(x)$, so Lemma~\ref{lem:rec-trapezoid} gives the error $E_i'\dB_i(x)$. Since $\log\dA_i$ is $c_i$-Lipschitz, the tail is at most $\dA_i(x)\dtail_i(c_i)\le\dB_i(x)\dtail_i(c_i)$ by Lemma~\ref{lem:rec-elementary}(c). The other two numerators are bounded similarly, using \eqref{eq:dig-strip} for $\phi$, Lemma~\ref{lem:rec-elementary}(d), $\E^i_x|W|\le\dk_ib_i$, and $\mathsf C'+|y|\le(\mathsf C'+1)\mathrm e^{|y|}$. For the ratio, we write $\mathsf T_i=\dB_i(1+\mathsf y_1)$, $|\mathsf y_1|\le\mathsf r_i$, and $\mathsf N=N+\mathsf y_2\dB_i$, $|\mathsf y_2|\le\mathsf r_{\mathrm n}$. Then $N/\dB_i-\mathsf N/\mathsf T_i=\mathsf y_1\mathsf N/\mathsf T_i-\mathsf y_2$, which is at most $\mathsf r_i|\mathsf N/\mathsf T_i|+\mathsf r_{\mathrm n}$ in absolute value, and hence at most the stated bound. This completes the proof of (a).

Part (b) follows as in (a), with $\dA_i=1$ and $\E(\mathsf C'+|W|)^2\le(\mathsf C'+b_i)^2$.

(c) We differentiate $\E\exp(c|x+bz|)=\mathrm e^{c^2b^2/2}\mathsf Q$ in $x$ and in $c$.

Part (d) follows from Lemma~\ref{lem:rec-elementary}(b), (e).
\end{proof}

The exact recursion is a sup-norm contraction by Lemma~\ref{lem:flow}(a), so errors add along the levels without amplification. In the computation this is not a separate estimate: every table entry is a ball, and its width passes through the exponentials, products and logarithms of the next level.

The functionals, namely the values of $Q$ and its integrals, come from a forward pass. Put $f^{\mathrm Q}_l:=1-\Psi_l'^2$, and $f^{\mathrm I}_l:=b_l^2-(2/c_l)(\dE_l-\Psi_l)$ for $c_l>0$, $f^{\mathrm I}_l(x):=b_l^2-\Var\Psi_{l+1}(x+b_lz)$ for $c_l=0$. Then
\begin{equation}\label{eq:dig-functionals}
  Q(s_l)=1-\E f^{\mathrm Q}_l(X_{s_l}),\qquad\int_{s_l}^{s_{l+1}}(1-Q)\dd w=\E f^{\mathrm I}_l(X_{s_l}).
\end{equation}
The first is the definition of $Q$. For the second, we have $\partial_{c_l}\Psi_l=(\dE_l-\Psi_l)/c_l$ (and $\frac12\Var$ at $c_l=0$), the chain rule through the lower levels gives $\partial_{c_l}\Psi_\kappa(0,\lambda)=\E[\partial_{c_l}\Psi_l(X_{s_l})]$, and \eqref{eq:dig-tangent} gives $\partial_{c_l}\Psi_\kappa(0,\lambda)=\frac12\int_{s_l}^{s_{l+1}}Q$. The same computation from $X_{s_l}=x$ gives $f^{\mathrm I}_l(x)=\int_{s_l}^{s_{l+1}}\E[1-u(w,X_w)^2\mid X_{s_l}=x]\dd w$, so $0\le f^{\mathrm I}_l\le b_l^2$.

Let $\pi_0$ be the outer trapezoid weights on the table of $\Psi_0$, and let $\pi_{i+1}(y)=\sum_x\pi_i(x)\mathsf h_{i+1}\varphi_{b_i}(y-x)\dA_i(y)/\mathsf T_i(x)$, folded to $y\ge0$ and restricted to the table of $\Psi_{i+1}$. Put $\mathrm{mass}_i=\sum\pi_i$. Let $\bar S$ bound $f$ on the strip of the step into level $l$.

\begin{lemma}\label{lem:rec-forward}
For $f=f^{\mathrm Q}_l$ with $S=1$, or $f=f^{\mathrm I}_l$ with $S=b_l^2$, so that $|f|\le S$ on $\R$, and with $\mathsf e=2\exp(-Z^2/2)S$,
\begin{align*}
  \Bigl|\E f(X_{s_l})-\sum_y\pi_l(y)f(y)\Bigr|\le{}&\sum_{i\le l-2}\mathrm{mass}_i\Bigl[S\,\frac{E_i'/\varpi_i+\dtail_i(c_i)+\mathsf r_i}{1-\mathsf r_i}+\mathsf e\Bigr]\\
  &+\mathrm{mass}_{l-1}\Bigl[\frac{E_{l-1}'\bar S+(\dtail_{l-1}(c_{l-1})+\mathsf r_{l-1})S}{1-\mathsf r_{l-1}}+\mathsf e\Bigr]+\mathsf o,
\end{align*}
where $\mathsf o$ is the term of the outer integral, of the same form, with $\mathrm{mass}=1$. One may take $\bar S=1+\bar{\dB}_{l-1}^2$ for $f^{\mathrm Q}_l$. For $f^{\mathrm I}_l$, with $\mathsf C_b=Y_{l-1}+\dk_{l-1}b_{l-1}+\dk_lb_l+\bar X_l$, one may take $\bar S=b_l^2+(2/c_l)(\mathsf C_b/\varpi_{l-1}+\mathsf C_b+K_{l-1})$ if $c_l>0$, and $\bar S=b_l^2+\mathsf f_{l-1}(\mathsf C_b+b_l)^2+\mathsf f_{l-1}^2(\mathsf C_b+b_l)^2$ if $c_l=0$.
\end{lemma}

\begin{proof}
Put $H_l=f$, $H_i(x)=\E^i_xH_{i+1}(x+W)$, $\mathsf J_i=\sum\pi_iH_i$, so that $\E f(X_{s_l})$ is the outer integral of $H_0$ and $|H_i|\le S$. We telescope the differences
\[
  \mathsf J_{i+1}-\mathsf J_i=\sum_x\pi_i(x)\Bigl[\sum_y\frac{\mathsf h_{i+1}\varphi_{b_i}(y-x)\dA_i(y)}{\mathsf T_i(x)}H_{i+1}(y)-H_i(x)\Bigr].
\]
The bracket is a ratio of truncated trapezoid sums against the true integrals, so Lemma~\ref{lem:rec-trapezoid} with \eqref{eq:dig-strip-H} bounds it for $i\le l-2$, where $H_{i+1}$ has the form $N/\dB_{i+1}$, and with $\bar S$ for $i=l-1$. The bound $\bar S$ on the strip follows from \eqref{eq:dig-strip}, \eqref{eq:dig-strip-H}, Lemma~\ref{lem:rec-elementary}(d), and $\E_{\mathrm t}|W|\le\dk b$.

It remains to treat the nodes $|y|>Y_{i+1}$ dropped from the table, for which we need $\sup_{|y|>Y_{i+1}}|H_{i+1}|\le\mathsf e$. By Lemma~\ref{lem:rec-elementary}(e), integrated over the level for $f^{\mathrm I}_l$, we have $|f(y)|\le2S\exp(-y^2/(2\tau_l^2))$. Since the drift $\kappa u$ has the sign of $X$, by Tanaka's formula $|X|$ is pathwise above the reflected Brownian motion from $|x|$. Hence $|H_i(x)|\le2S\E\exp(-(x+B)^2/(2\tau_l^2))\le2S\exp(-x^2/(2\tau_i^2))$, where $B$ has variance $s_l-s_i$, and $\tau_l^2+s_l-s_i=\tau_i^2$. With $Y_i\ge Z\tau_i$ this is $\mathsf e$, and the proof is complete.
\end{proof}

The sums of the recursion are evaluated by products of ball polynomials, and every error term above is evaluated in ball arithmetic and added to the radius. The evaluation also verifies, in balls or exact rationals, the nesting of the lattices, $N_i^2\mathsf h_i^2\ge Z^2\tau_i^2$ where $Y_i=N_i\mathsf h_i$, $\varpi_i>0$, $\mathsf r_i<1/2$, $\mathsf q<1$ for every tail, and that $c_i$ is nondecreasing. The forward pass uses $4\exp(-Z^2/2)S$, unweighted, in place of $\mathrm{mass}_i\mathsf e$, which absorbs a mass above $1$. Floating point chooses $\mathsf h_i,N_i,a_i,J_i$ and has no other role.

\subsection{What is computed}\label{ssec:computed}
All certified numbers are outputs of FLINT/Arb \cite{Arb} ball arithmetic, through python-flint 0.9.0, at $160$ bits. Every parameter reaches a ball as an exact rational. Floating point proposes trials, grids, table sizes, the function $\vartheta$ and anchors. It enters no bound: every proposed object is rechecked in balls or exact rationals before use. A bound written here with $\le$ or $\ge$ is rounded in the safe direction, and a printed ball contains the unrounded value. Other decimals, such as the entries of Tables~\ref{tab:dig-upper} and~\ref{tab:dig-low}, are rounded to nearest. Acceptance uses ball comparisons only.

The trial nodes have $31$ levels on $[0.9555,0.9785]$ and $25$ levels outside, down to $t_k$ about $2\cdot10^{-9}$, with mesh $1.23\cdot10^{-5}$ near $m=0.9667$. The levels are cut at between $177$ and $628$ nodes $s_i$. The $48$ SK nodes of Theorem~\ref{thm:bracket-window} and the $34$ further SK nodes of Theorem~\ref{thm:no-low-well} use $8$-step trials, the former cut at between $29$ and $353$ nodes. The value at $0.974$ uses a $12$-step trial cut at $215$ nodes.

We compute the two values in Corollary~\ref{cor:load-bound} as follows. Let $\mathsf f(s)=\E\tanh^2(\sqrt s\,z)$, $\alpha=2$, and $(\gamma,y_{\mathrm h})=(2,0.35)$ or $(4.44,0.5)$. It is enough that $y/(1-y)^2<\gamma\mathsf f(\gamma\alpha y)$ on $(0,y_{\mathrm h}]$. On $(0,1/100]$, the bound $\tanh^2s\ge s^2-\frac23s^4$ gives $\mathsf f(x)\ge x-2x^2$, so it is enough that $\gamma^2\alpha(1-2\gamma\alpha/100)>(1-1/100)^{-2}$. For $[1/100,y_{\mathrm h}]$ we use $400$ cells. Since both sides increase in $y$, on each cell we compare the left side at the right end with a lower bound of the right side at the left end, namely a lower Riemann sum in $|z|\le8$, with step $1/200$ and Gaussian masses in balls.

Code and certificates are in the repository given under Code and data. Every certified number has been rebuilt from a clean start, and the computed values agree with the stored certificates. Two separately written checkers, also written by AI, share only Arb with this code, each with its own remainder bounds and its own grids.

The first recomputed the pair at $\alo$, the pair of Theorem~\ref{thm:certified-wells}(b), the worst cell at $\ahi$, the value at $0.974$, and its own recursions at $22$ of the $164$ trial nodes, and it reran the mesh logic over all $35$ load intervals. All balls overlap. The second evaluated Theorem~\ref{thm:recursion-bound} at all $82$ SK nodes on the stored rational trials, where its values of $\dP_m$ overlap the stored ones and its lower bounds are at least the stored ones. With its own values it passes all cells of Theorem~\ref{thm:no-low-well}, and it confirms the two computations behind Corollary~\ref{cor:load-bound}. At the other $142$ trial nodes the recursion has been reproduced only by the rebuild, not by separate code.