On the Log-Concavity of the Riemann Xi Kernel

The Riemann Xi function admits the representation ( Xi(t) = int_0^infty Phi(u)cos(tu),du ) where ( Phi ) is a positive, even, integrable function. By a classical theorem of P’olya (1927), if ( logPhi ) is concave on ( [0,infty) ), then ( Xi ) has only real zeros, which is equivalent to the Riemann Hypothesis. We prove that the dominant term of ( Phi ) has strictly negative second logarithmic derivative for all ( u geq 0 ), reducing the full log-concavity to a quantitative tail estimate. We verify this estimate by rigorous interval arithmetic (5000 certified subintervals on ( [0, 1/2] ) at 80-digit precision, with the complement handled analytically). The entire argument is formalised in the Lean~4 proof assistant with the Mathlib library.