Ramanujan's prime-counting inequality holds for all x ≥ 38,358,837,683

Ramanujan observed that π(x)² < (ex/log x)·π(x/e) for all sufficiently large x. Dudek and Platt showed, assuming the Riemann hypothesis, that the last counterexample is x = 38,358,837,682. Unconditionally the inequality was known for 38,358,837,683 ≤ x ≤ e^103 (Johnston) and for x ≥ e^3158.442 (Axler). We close the gap: the inequality holds unconditionally for every x ≥ 38,358,837,683. The proof uses no verification of the Riemann hypothesis beyond the height 3·10¹² established by Platt and Trudgian. It combines a smoothed explicit formula of Büthe's type with three new explicit inputs: a log-free zero-density estimate near the 1-line, obtained by reworking Bellotti's argument with a sharp asymptotic evaluation of the Barban–Vehov mean square; a height-dependent zero-free region, obtained by evaluating the inequality of Bellotti, Trudgian and Yang exactly; and a repulsion lemma showing that two hypothetical zeros close to the 1-line cannot lie close to each other in height. All constants and auxiliary bounds are certified in rigorous interval (ball) arithmetic; the final scan over 57 ≤ log x < 3159 is run in double precision, with an explicit rounding analysis. Along the way we record several corrections to the explicit inputs we use, none of which affects the published main results. AI involvement: this work was carried out with substantial assistance from Claude (Anthropic), which performed most derivations, wrote and ran the certification code, and drafted the manuscript under the author's direction. Code, certificates and logs are included.