Bounds for the smallest limit point of the areal Mahler measure of totally positive algebraic integers

Pritsker's areal analog of the Mahler measure replaces the integral of log|P| over the unit circle by its integral over the unit disc with respect to normalized area. For an algebraic number α of degree n whose minimal polynomial P in Z[x] is primitive with positive leading coefficient, let N0(α) = ‖P‖01/n. Flammang proved that N0(α) ≥ 1.380047 for every totally positive algebraic integer α outside an explicit finite set. We prove that all but finitely many totally positive algebraic numbers satisfy N0(α) > 1.3830134, and that infinitely many totally positive algebraic integers satisfy N0(α) < 1.3842933. So the smallest limit point of the values of N0 on totally positive algebraic integers, and the essential minimum, lie between 1.3830134 and 1.3842933; we are not aware of an earlier upper bound. The lower bound comes from an auxiliary function with Flammang's polynomials and a logarithmic energy term, and the upper bound from a measure that satisfies a criterion of Smith, as in our two papers on the classical Mahler measure of totally positive algebraic integers. Both certificates are verified in ball arithmetic. We also proved in Lean, without hypotheses, a lower bound with the slightly smaller constant 1.3823468, and the upper bound, assuming the theorem of Smith that it uses. The certificates, the checking programs with their logs, the modified certificates used to test the programs, the Lean proofs, and the programs that produced the certificates are archived at doi:10.5281/zenodo.23541254. They are also available at github.com/tejasvi/areal-mahler-measure-v3. Change note. Versions 1 and 2 stated that two transcriptions of Flammang's Table 2 agree; they differ in row 58, which neither certificate uses; no bound changes.