All even logarithmic differences of Boros–Moll coefficients

Abstract

We prove a conjecture posed by Chen and Gu in 2008 by showing that every admissible even-order difference of the logarithms of a Boros–Moll coefficient row is strictly negative. The fourth-order case gives the conjectured ratio log-concavity, including the endpoint ratios. We establish the stronger continuous statement that every even derivative of an explicit interpolation is negative. The proof writes the coefficients as a binomial factor times a Laplace transform. The exponentially weighted kernel is decreasing, which yields a Bernstein function. An elementary derivative-sign argument and the gamma recurrence then prove all orders at once. Version 2 replaces the earlier fourth-order argument with a self-contained analytic proof of all admissible even orders. The support archive contains source/build files and historical finite-range Lean sources. The all-orders analytic proof is not formalised in Lean; no computation is required for the proof.