Certified psi bound up to 13,631,488 with theta endpoint

Let $\theta(x)=\sum_{p\leq x}\log p$ and $\psi(x)=\sum_{p^m\leq x,\ m\geq1}\log p$, where $p$ ranges over primes and $m$ over positive integers. This finite certificate establishes

and, for every integer $n$ with $1000<n\leq13631488$,

The endpoint estimate supplies the initial upper bound for $\theta$ in the next contiguous interval. Both statements are unconditional. The endpoints and the rational upper bound are chosen for this formal verification of the finite part of the Rosser-Schoenfeld estimate; they are not separately numbered claims in the original paper. This certificate alone does not cover integers above 13631488.