A lower bound for the smallest limit point of the absolute Mahler measure of totally positive algebraic integers

Let Ω(α) = M(α)1/deg α be the absolute Mahler measure of an algebraic number α, so that log Ω(α) is its absolute logarithmic Weil height. By work of Smyth, every number in [1.7273…, ∞) is a limit point of the values of Ω on totally positive algebraic integers, and Flammang proved that Ω(α) ≥ 1.722069 for every totally positive algebraic integer α outside an explicit finite set. We prove that all but finitely many totally positive algebraic numbers α satisfy Ω(α) > 1.7234615. Hence the smallest limit point of these values lies between 1.7234615 and 1.7274, and all but finitely many totally real algebraic numbers β satisfy log Ω(β) > 0.2721673. The proof combines Smyth's method of auxiliary functions with the logarithmic energy term that Orloski, Talebizadeh Sardari and Smith derived from the integrality of discriminants. The auxiliary function uses x and eighteen of Flammang's polynomials, and the reference measure has a piecewise linear density, so that its potential and energy have closed forms. Two separately written programs verify the resulting inequality on the positive half-line in ball arithmetic. The lower bounds for totally positive numbers are also proved in the Lean proof assistant, under one assumption from potential theory, with the checks of the certificate run as compiled code. The certificate, the two checkers, their tests, the programs that produced the certificate and the Lean files are archived at doi:10.5281/zenodo.23539851 and available at github.com/tejasvi/totally-positive-mahler-measure-v2.