2026/07/31 by Jinhui Li, Beibei Xiong, Zhengfeng Yang
Computer Science · #cs.SC
arxiv created 2026/07/31 · arxiv updated 2026/08/03
The Dittert conjecture states that the Dittert functional on nonnegative n× n matrices whose entries sum to n is uniquely maximized by the uniform matrix. We prove the conjecture in dimension 4. More precisely, let K4 be the simplex of nonnegative 4×4 real matrices whose entries sum to 4, let U4 be the uniform matrix, and let ϕ denote the Dittert functional. We establish (61)/(32)-ϕ(A)≥ (1)/(52)‖ A-U4‖F2 for every A∈ K4. Consequently, U4 is the unique maximizer of ϕ on K4. The proof reduces to certifying the nonnegativity of a structured quartic polynomial in sixteen variables on a simplex. We construct an exact rational constrained sum-of-squares certificate using an agent-guided symbolic-numeric procedure that combines template selection with sequential rational recovery. The main SOS consists of 152 positively weighted rational squares, while each of the 136 smaller SOS blocks consists of 16 such squares. Exact LDLT decompositions certify positivity, and exact coefficient comparison over ℚ verifies the complete polynomial identity. The resulting exact certificate is formally verified using the Lean proof assistant.