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

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

one has

This is the middle segment 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): the explicit lower bound for $\theta$ that is valid for every $t\ge 1340$.

The range here is deliberately finite. The universal statement $t\ge 1340$ is the platform theorem TaoFivePrimes.rosser_schoenfeld_theta_lower_analytic; it decomposes into exactly three segments. Below $1420$ the sharper elementary bound $t-2\sqrt t<\theta(t)$ is already available as the proved platform theorem TaoFivePrimes.rosser_schoenfeld_theta_lower_finite (Rosser--Schoenfeld, Theorem 4, finite range $255\le t\le 1420$), and above $10^{10}$ the two-sided Chebyshev estimate of the platform input TaoFivePrimes.schoenfeld_psi_error_large already forces (3.14), because $\psi(t)-\theta(t)\le 2\sqrt t\log t$ is available in Mathlib as Chebyshev.psi_sub_theta_le and $(19/40)\sqrt t>2(\log t)^2$ on that range. What remains, and what this theorem isolates, is the genuinely finite computational range $(1420,10^{10}]$

Formalization Note Chebyshev.theta is Mathlib's $\theta$ function on $\mathbb{R}$. The upper endpoint $10^{10}$ is not a source constant: it is the threshold at which the elementary comparison $(19/40)\sqrt t>2(\log t)^2$ becomes provable from $\log t\le 8\,t^{1/8}$, so that the Schoenfeld input can take over. The range $255\le t\le 1420$ of the proved finite node is quoted as-is from the platform.