Rosser--Schoenfeld (1962), Theorem 4, eq. (3.14): the finite range $1420 \le t \le 10^{9}$

Rosser--Schoenfeld (1962), Theorem 4, eq. (3.14), finite part of the middle range. Let $\theta(t)=\sum_{p\le t}\log p$ over primes $p$. For every real $t$ with

one has

This is the finite part of inequality (3.14) of Rosser and Schoenfeld, Approximate formulas for some functions of prime numbers, Illinois J. Math. 6 (1962), 64--94, Theorem 4 (printed p. 70).

Why this node exists. The sibling theorem TaoFivePrimes.rosser_schoenfeld_theta_lower_analytic_mid carries the whole range $1420\le t\le10^{10}$ as a single finite obligation, and above $10^{10}$ the published node TaoFivePrimes.schoenfeld_psi_error_large already forces (3.14). Splitting the middle range at $10^{9}$ makes the finite obligation ten times smaller and leaves the analytic part entirely to the $\psi$ input: on $t\ge10^{9}$ the two-sided estimate $|\psi(t)-t|\le t/(40\log t)$ together with Mathlib's Chebyshev.psi_sub_theta_le, $\psi(t)-\theta(t)\le 2\sqrt t\log t$, reduces (3.14) to the elementary comparison $(19/40)\sqrt t>2(\log t)^2$, which holds on that range because $\log t\le 16\,t^{1/16}$ (four nested square roots) and $\sqrt[8]{t}\ge13.3$.

Why $10^{9}$ and not $10^{8}$. The threshold is a seam, not a feature: $10^{9}$ is a round constant for which $(19/40)\sqrt t>2(\log t)^2$ is still provable from the explicit logarithmic bound used in the sibling reduction. The genuinely finite range $1420<t\le10^{9}$ is what a future certificate has to cover.

Formalization Note Chebyshev.theta is Mathlib's $\theta$ function on $\mathbb{R}$. The statement is a range restriction of the existing platform theorem TaoFivePrimes.rosser_schoenfeld_theta_lower_analytic_mid; no new mathematics is claimed beyond the range split, which is a formalization choice and not a separately numbered statement in the source.