An explicit bound below 2/π for the maximum term of an entire function

For a transcendental entire function f(z) = ∑ akzk, let μ(r) = maxk |ak|rk be its maximum term and M(r) its maximum modulus on |z| = r. Erdős asked for the largest possible value B of lim inf μ(r)/M(r) as r → ∞ (Erdős problem #513). An argument of Clunie gives B ≤ 2/π = 0.636619…, and in 1964 Clunie and Hayman proved B ≤ 2/π − c for an absolute constant c > 0, which they did not compute. The lower bound B > 0.5850788 is due to Sothanaphan, who improved the parameters of a construction of He and Tang. We prove B ≤ 0.63005. The proof bounds M(r) from below by duality: trigonometric polynomials are tested against the Fourier coefficients of f(reiθ) in a finite window. Two consecutive radii at which the central index jumps involve three consecutive vertices of the Newton polygon of log|ak|. If the two gaps between these vertices are equal, testing f at both radii leads to a problem in six real parameters. If they differ, a single radius is used, and averaging over roots of unity leads to a problem in seven parameters for each value p ≥ 2 of the larger gap divided by the greatest common divisor of the two gaps. Both problems are bounded by branch and bound, with dual vectors certified in ball arithmetic. Two independently written programs check the certificates, which have 176,240 leaves in the equal-gap case and 37,198 in the unequal-gap case. The theorem also has a proof in the Lean 4 proof assistant, in which a checking program written and proved correct in Lean checks the certificates; every check is evaluated by the Lean kernel itself. The certificates, both checkers, the programs that produced them and the Lean files are archived at doi:10.5281/zenodo.23548812 and available at github.com/tejasvi/maximum-term-bound-v3.