An explicit Mertens-product bound at the Morrill–Platt threshold, with applications to Robin's inequality

Let F(x) = Σ_{p≤x} log(p/(p−1)) − γ − log log θ(x). We prove that F(x) ≤ 1.3064373·10⁻⁸ for every x ≥ X₀ = 29 996 208 012 611; Morrill and Platt verified Robin's inequality σ(n) < e^γ n log log n for all 5040 < n ≤ X₀# (their Theorem 5 and Corollary 2). The proof uses the explicit formula for ∫₀^x ψ(t) dt, the verification of the Riemann hypothesis up to height 3·10¹², and published explicit bounds for primes (Rosser–Schoenfeld 1962, Büthe 2018, Platt–Trudgian 2021), which are used as published; the numerical constants computed here are certified with interval arithmetic. With the computation of Morrill and Platt and known elementary reductions (Solé–Planat, Hertlein, Axler, Saouter), this single constant gives: Robin's inequality holds for every n > 5040 with 2²⁶ ∤ n, hence for every 26-free n > 5040 (the previous result known to us is 21-free); it holds for every n > 5040 not divisible by some prime p ≤ 76 543 853; and σ(n) < (1 + 1.3065·10⁻⁸) e^γ n log log n for every n > 5040 (previously known to us: 1 + 3.15367·10⁻⁷). With the verified range of Morrill and Platt, 26-free is the limit of this method. These statements concern all integers; the least counterexample to Robin's inequality, if it exists, is already known to satisfy much stronger conditions, so they give no information on the Riemann hypothesis itself.