Explicit sign changes in comparative prime number theory: computer-assisted proofs with checkable certificates

This research report gives rigorous, computer-assisted proofs of several explicit results on oscillations of arithmeticsums, each with a checkable certificate and a verification path that does not depend on the author's software. Main results: (i) an explicit region where the error term of Mertens' first theorem is negative (problem 14 of the list ofHamieh, Kadiri, Martin and Ng); (ii) a sign change in the prime race 24k+1 versus 24k+11 below 2.79·10^48, improving thebound 10^353 of Ford and Hudson; (iii) an explicit negative value of Shanks' sum Σ λ(n)χ_{−4}(n) and an unconditionalproof, by the classical method of Landau and Ingham, that it changes sign infinitely often; (iv) certified counterexamplesto five strict inequalities of Conjecture 1.3 of Z.-W. Sun, explicit failures of his Hypothesis 1.2 for Q(i) and Q(√−2),an explicit height for violations of his Hypothesis 1.1, and an unconditional proof, by Selberg–Delange asymptotics, thateach of the seventeen eventual inequalities of his Conjecture 1.2 fails infinitely often; (v) three explicit regions withπ(x) > li(x), near 10^3127.6, 10^6217.1 and 10^8045.6; (vi) under GRH, a complete classification of the pairs (q,a) forwhich the integrated prime race ∫(φ(q)π(t;q,a) − li t)dt is eventually negative (PIMS problem 23; LI needed only for the"only if" direction), with a certified correction of one omission in Table 1 of Zhao (2025). All numerical claims used in proofs are backed by ball (interval) arithmetic with every error term bounded. Theaccompanying package contains the certificates, short checkers (Python + python-flint/Arb), logs and SHA-256 sums; thereport lists, for every result, what can be checked by hand and what requires a computer. The author is an independentresearcher; novelty statements mean "not found in the literature consulted", and corrections are welcome.