The Dittert conjecture states that the Dittert functional on nonnegative $n\times n$ matrices whose entries sum to $n$ is uniquely maximized by the uniform matrix. We prove the conjecture in dimension $4$. More precisely, let $K_4$ be the simplex of nonnegative $4\times4$ real matrices whose entries sum to $4$, let $U_4$ be the uniform matrix, and let $φ$ denote the Dittert functional. We establish $\frac{61}{32}-φ(A)\ge \frac{1}{52}\|A-U_4\|_F^2$ for every $A\in K_4$. Consequently, $U_4$ is the unique maximizer of $φ$ on $K_4$. The proof reduces the problem to an exact certification of the nonnegativity of a structured quartic polynomial in sixteen variables on a simplex. We develop a symbolic-numeric procedure for constructing an exact rational constrained sum-of-squares certificate. The procedure combines adaptive template selection with sequential rational recovery to handle singular Gram matrices and coupled SOS blocks arising from the constraint structure. The final certificate consists of a main SOS with $152$ positively weighted rational squares and $136$ smaller SOS blocks, each containing $16$ such squares. Exact $LDL^T$ decompositions and coefficient comparison over $\mathbb{Q}$ certify the polynomial identity. The resulting exact certificate is formally verified using the Lean proof assistant.

翻译：暂无翻译