{"id":"palomar/PALOMAR-2026-10-27-000009","url":"https://github.com/tejasvi/lean4body-optimal-bound/tree/4967a62ec6f41d075d1808bbfd091927bcfe9c7b","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-27-000009-v1.json","repo":"https://github.com/tejasvi/lean4body-optimal-bound","tags":["math.DS","math-ph","msc:70F10","msc:70F15","msc:65G40"],"score":0,"title":"The optimal Hessian bound for convex four-body central configurations","trust":"high","domain":"math.DS","source":"palomar","authors":["Tejasvi Singh Tomar"],"reviews":0,"subject":"math.DS","summary":"A Lean 4 and Mathlib formalization of Conjecture 7.3 of arXiv:2609.35632 on the central configurations of the planar Newtonian four-body problem. At every strictly convex central configuration of four positive masses, the Hessian form Q of U + (λ/2)I is at least two thirds of its radial part K, and strictly so wherever K is positive. In the notation of the paper this is λ_max(G) < 1/3 for the explicit 2×2 matrix G of its Proposition 3.5, and by its Proposition 7.2 the constant 2/3 is optimal. It sharpens Theorem B of the paper, Q ≥ K/4. The definitions and the reduction to the normal form of…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-27","reactions":{},"formalized":true,"formalizes":[{"title":"Uniqueness of four-body convex central configurations for all masses","identifier":"arXiv:2609.35632","relationship":"formalizes"}]}