Rédiger un PREreview

The Riemann Xi function admits the representation Ξ(t) = ∫₀^∞ Φ(u)cos(tu) du where Φ is a positive integrable function on [0,∞). We prove that Φ is strictly log-concave (TP₂) on [0,∞): (log Φ)″(u) < 0 for all u ≥ 0. We give two independent proofs: (i) a computational proof via rigorous interval arithmetic (5000 certified subintervals at 80-digit precision), and (ii) a purely analytic proof via a convex potential decomposition φₙ = e−Vₙ with Vₙ″ > 0, requiring no computation. The analytic proof appears to be the first pen-and-paper log-concavity result for a kernel in the Jacobi theta function family. The perturbation from higher-order terms uses only 4.3% of the available log-concavity budget, leaving a 95.7% margin. Log-concavity (TP₂) is a necessary condition for the Riemann Hypothesis; the passage to the full Laguerre–Pólya condition (TP∞) remains open. Both proofs are formalised in the Lean 4 proof assistant.