\section{The certified interval inclusions}
\label{q:app:certificate}
Each row of Table~\ref{q:tab:certificate} is one proved inclusion: over the rational box on $(Q,A,B)$ shown, with $h\in(0,\tfrac1{600}]$, $u\in(0,\tfrac1{20}]$ and the prefactor intervals of~\eqref{q:eq:parameters}, the indicated normalised derivative lies in the enclosure. The sign or margin required by Lemma~\ref{q:lem:corridor} is read off the relevant endpoint; the enclosures are conservative, so the actual margins are larger than the required ones (for instance the lower $A$ entry slab certifies $R_A\ge0.278>\tfrac14$, the lower $B$ entry slab $R_B\ge1.389>1$ and the lower $Q$ entry slab $R_Q\ge0.1808>\tfrac1{10}$). The checker operates on a rational expression tree with atoms for the thirteen variables; the interval evaluation is proved sound for every real point of the box, the endpoint arithmetic is verified by Lean's kernel, and the identification of the expression trees with~\eqref{q:eq:RA}--\eqref{q:eq:RQ} is a separately proved polynomial identity.

\begin{table}[htb]
\centering\small\renewcommand{\arraystretch}{1.15}
\caption{The eighteen certified inclusions (enclosures rounded outward to four digits).}
\label{q:tab:certificate}
\begin{tabular}{llllll}
\toprule
name & function & $Q$ & $A$ & $B$ & certified enclosure\\
\midrule
outer $A$ lower & $R_A$ & $[1/4,1]$ & $3$ & $[1,3]$ & $[0.7830,\ 1.0701]$\\
outer $A$ upper & $R_A$ & $[1/4,1]$ & $5$ & $[1,3]$ & $[-1.2372,\ -0.9099]$\\
outer $B$ lower & $R_B$ & $[1/4,1]$ & $[3,5]$ & $1$ & $[3.4661,\ 8.1284]$\\
outer $B$ upper & $R_B$ & $[1/4,1]$ & $[3,5]$ & $3$ & $[-16.025,\ -7.4965]$\\
outer $Q$ lower & $R_Q$ & $1/4$ & $[3,5]$ & $[1,3]$ & $[0.9653,\ 1.0079]$\\
outer $Q$ upper & $R_Q$ & $1$ & $[3,5]$ & $[1,3]$ & $[-74.785,\ -7.9000]$\\
inner $A$ lower & $R_A$ & $[1/2,3/4]$ & $7/2$ & $[3/2,5/2]$ & $[0.3327,\ 0.5751]$\\
inner $A$ upper & $R_A$ & $[1/2,3/4]$ & $9/2$ & $[3/2,5/2]$ & $[-0.6774,\ -0.4149]$\\
inner $B$ lower & $R_B$ & $[1/2,3/4]$ & $[7/2,9/2]$ & $3/2$ & $[1.8653,\ 4.6560]$\\
inner $B$ upper & $R_B$ & $[1/2,3/4]$ & $[7/2,9/2]$ & $5/2$ & $[-7.0657,\ -3.1880]$\\
inner $Q$ lower & $R_Q$ & $1/2$ & $[7/2,9/2]$ & $[3/2,5/2]$ & $[0.1807,\ 0.7258]$\\
inner $Q$ upper & $R_Q$ & $3/4$ & $[7/2,9/2]$ & $[3/2,5/2]$ & $[-8.1258,\ -2.2276]$\\
entry $A$ lower & $R_A$ & $[1/4,1]$ & $[3,7/2]$ & $[1,3]$ & $[0.2780,\ 1.0701]$\\
entry $A$ upper & $R_A$ & $[1/4,1]$ & $[9/2,5]$ & $[1,3]$ & $[-1.2372,\ -0.4149]$\\
entry $B$ lower & $R_B$ & $[1/4,1]$ & $[7/2,9/2]$ & $[1,3/2]$ & $[1.3891,\ 7.1225]$\\
entry $B$ upper & $R_B$ & $[1/4,1]$ & $[7/2,9/2]$ & $[5/2,3]$ & $[-15.059,\ -3.1298]$\\
entry $Q$ lower & $R_Q$ & $[1/4,1/2]$ & $[7/2,9/2]$ & $[3/2,5/2]$ & $[0.1807,\ 1.0056]$\\
entry $Q$ upper & $R_Q$ & $[3/4,1]$ & $[7/2,9/2]$ & $[3/2,5/2]$ & $[-50.162,\ -2.2276]$\\
\bottomrule
\end{tabular}
\end{table}