A lower bound for the essential minimum of the Zhang–Zagier height

For an algebraic number α let h(α) be its absolute logarithmic Weil height, and let hZ(α) = h(α) + h(1 − α). The essential minimum of hZ is the supremum of the numbers H for which only finitely many algebraic numbers satisfy hZ(α) ≤ H. Zagier showed that it is at least ½ log((1 + √5)/2) = 0.2406059…, and the best lower bound so far is 0.24874, due to Flammang. We prove that the essential minimum is at least 0.24982933. The proof combines Smyth's method of auxiliary functions, here with five integer polynomials in z(1 − z), with a logarithmic energy term relative to a measure on the circles |z| = 1 and |1 − z| = 1. Resultants and discriminants of minimal polynomials are nonzero integers. They bound the polynomial terms and the energy term, and a condition on the degrees absorbs the leading coefficients, so the argument applies to all algebraic numbers. A superharmonicity argument reduces the positivity of the auxiliary function to the unit circle, where two separately written programs verify it in ball arithmetic for a certificate with exact rational data. The certificate, the two checkers and the programs are archived at doi:10.5281/zenodo.23512782 and available at github.com/tejasvi/zhang-zagier-lower-bound.