Certificate inequality for the primorial sample points (m = 4..65)

Let $P_m = p_1 p_2 \cdots p_m$ be the product of the first $m$ primes (the primorial), so that $P_m / \varphi(P_m) = \prod_{i=1}^{m} p_i/(p_i-1)$ is the totient ratio at the primorial sample point. The table Qpt m holds these ratios; the table rll m holds certified rational lower bounds for $\log\log P_m$.

The theorem certifies, for every $4 \le m \le 65$, the rational inequality

where $R_m = \mathrm{rll}(m)$, $Q_m = \mathrm{Qpt}(m)$, and $1.78107237$ is a certified lower bound for $e^{\gamma}$.

Because $e^{\gamma} \ge 1.78107237$, $\log\log P_m \ge R_m$, and $t \mapsto 1.78107237\,t + 2.50637/t$ is increasing for $t > \sqrt{2.50637/1.78107237} \approx 1.19$ while $R_m \ge 1.67$ throughout the range, this is exactly the pointwise Rosser--Schoenfeld totient bound

evaluated at the 62 sample points $n = P_m$, $4 \le m \le 65$. It is the arithmetic core of the finite verification: the remaining sample points $n \le p_4\cdots p_4$ are handled separately by a monotonicity argument.