Rosser–Schoenfeld upper bound $\vartheta(y) < y + y/(2\log y)$ for $y \ge 563$

Let $\vartheta(y) = \sum_{p \le y} \log p$ be Chebyshev's function (sum over primes $p \le y$, natural logarithm). For every real $y \ge 563$,

This is the upper half of Rosser–Schoenfeld's Theorem 4 (which states it on a wider range of $y$), restricted to the range $y \ge 563$ in which Harvey–van der Hoeven quote it in the proof of their Lemma 5.1. Together with the matching lower bound $y - y/(2\log y) < \vartheta(y)$ it gives IntMul.HvdH.rosser_schoenfeld_thm4.

Formalization note: Chebyshev.theta is Mathlib's $\vartheta$ on $\mathbb{R}$; since $y \ge 563$, $\log y > 0$ and no junk values arise. The inequality is strict.