The sharp Hessian bound for convex four-body central configurations

In a previous paper (arXiv:2609.35632) we proved that the planar four-body problem has exactly one convex central configuration for each choice of positive masses and each cyclic order of the bodies, by proving that these configurations are nondegenerate. Here we prove the sharp form of this nondegeneracy: at every convex central configuration, the Hessian of the potential on a level set of the moment of inertia exceeds two thirds of its radial part. The constant 2/3 is optimal; it is approached by isosceles trapezoids in which the two masses on one of the parallel sides tend to zero. We give two independent computer-assisted proofs of an equivalent inequality for the largest eigenvalue of a 2×2 matrix that depends only on the shape of the configuration, and one of them is formalized in the Lean proof assistant. Besides the paper, the record contains the programs and data for the computer-assisted part of the paper's first proof. That part covers the configurations with a relatively short side (roundness at most 3/4, in the paper's terms), while Section 4 of the paper treats the others by hand. The programs run with Python and the python-flint library, and one of them also needs SymPy. README.md explains how to check and run them. In our runs the longest of the checks took about 11.5 hours with up to nine processes at a time, needed more than 72 GiB of memory, and completed with 120 GiB available. Section 9 of the paper also describes a formal proof in Lean of the main theorem of arXiv:2609.35632. The repositories of both formal proofs are listed under Related works. Mathematics Subject Classification (2020): 70F10, 70F15, 65G20, 68V20.