An algebraic integer is totally positive if all roots of its minimal polynomial are real and positive. The average of these roots is its trace divided by its degree, and the trace constant is the smallest value at which such averages accumulate. Schur, Siegel and Smyth bounded it from below, and Smith showed that it is below 1.89831. The best earlier bounds were 1.80220, reported by Giraudin from floating-point checks, and 1.8117251, by Pinho. Here the range narrows to between 1.8022032 and 1.8070809, and the Lean proof assistant checks both bounds, the upper one assuming Smith's theorem.
Abstract
The Schur–Siegel–Smyth trace constant C86 is the lower limit of tr(α)/deg(α) over totally positive algebraic integers α. We prove 1.8022032 < C86 < 1.8070809. For the upper bound we exhibit a measure on [0, 6] that satisfies the hypotheses of Smith's theorem on limits of distributions of conjugates, which we check with the help of 21 integer polynomials. This improves the upper bounds 1.8216 of Orloski and Talebizadeh Sardari and 1.8117251 of Pinho. The lower bound comes from the method of Orloski, Talebizadeh Sardari and Smith with fifteen polynomials, three of them of degree 10 found by McKee and Smyth. It is larger than the bound 1.80220 reported by Giraudin, whose verification evaluates its bounds in floating-point arithmetic with fixed safety margins; ours encloses every rounding error. For each bound, two separately written programs check the certificate in ball arithmetic. Both bounds are also proved in Lean 4, the upper bound under the assumption of Smith's theorem. We also give evidence that certificates of this kind cannot lower the upper bound much further without integer polynomials of high degree.
Illustration of the certificate for the upper bound. Top: the certificate's measure μ₀ on [0, 6], drawn as its mass in 600 equal intervals divided by their length, so that area is mass; its piecewise linear density is a weighted sum of hat functions on 2,325 nodes, 1,510 of them with nonzero weight, and its support lies in [0.054, 5.227] and has many gaps. Smith's theorem is applied to μ = (1 − ε)μ₀ + εω with ε = 1/100000, where ω is the equilibrium measure of [0, 6], and the bound is the mean of μ, 1.80708083…, rounded up to 1.8070809. Bottom: log₁₀ h, where h(x) = (1 − ε)(U(x) − Σ b_Q log|Q(x)|) + ε log(3/2), U is the potential of μ₀ and Q runs through the certificate's 21 integer polynomials with weights b_Q; the panel runs from 10^(−6.5) at the bottom up to 10, where the curve is cut off. h rises to infinity at the 102 real roots of the polynomials, marked by the yellow dots, and between the spikes, where μ₀ carries mass, it stays near 4·10⁻⁶, the value 4.05·10⁻⁶ of the term ε log(3/2), dipping to about 3.6·10⁻⁶ near x = 0.744. The paper's two programs prove h ≥ 0 on [0, 6], which together with a degree condition and one integral condition for each polynomial gives the bound through Smith's theorem. The picture is computed in floating point from the certificate's exact data.
