AI 中文总结
该研究通过智能体引导的符号-数值方法构造精确平方和证书，在4维下证明Dittert猜想，确定均匀矩阵为对应Dittert泛函的唯一最大值点，且证书经Lean形式化验证。
AI 中文摘要
Dittert猜想指出，对于元素和为n的非负n×n矩阵，Dittert泛函在均匀矩阵上达到唯一最大值。我们在4维下证明了该猜想。更确切地说，设K₄为元素和为4的非负4×4实矩阵构成的单纯形，U₄为均匀矩阵，φ表示Dittert泛函。我们对所有A∈K₄，证明了61/32 - φ(A) ≥ (1/52)||A - U₄||_F²，由此可得U₄是φ在K₄上的唯一最大值点。该证明归结为在单纯形上证明一个含16个变量的结构化四次多项式的非负性。我们采用智能体引导的符号-数值方法构造精确有理约束平方和（SOS）证书，该方法结合了模板选择与序贯有理恢复。主SOS包含152个带正权重的有理平方，136个较小的SOS块各包含16个此类平方。精确LDLᵀ分解用于证明正定性，在ℚ上的精确系数比较用于验证完整多项式恒等式。所得精确证书通过Lean证明助手进行形式化验证。
英文摘要
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.
