Overview
Research has provided a proof for the Dittert conjecture in dimension 4. This conjecture posits that the Dittert functional, when applied to nonnegative $n \times n$ matrices whose entries sum to $n$, is uniquely maximized by the uniform matrix. The proof establishes a specific inequality for dimension 4, demonstrating that the uniform matrix $U_4$ is the sole maximizer of the Dittert functional $\phi$ on the simplex $K_4$ of nonnegative $4 \times 4$ real matrices with entries summing to 4.
Research Context
The Dittert conjecture concerns the properties of the Dittert functional. For $n \times n$ matrices, the conjecture states that the uniform matrix is the unique maximizer of this functional under specific conditions: the matrices must be nonnegative, and their entries must sum to $n$. The current work focuses on the $n=4$ case, specifically the simplex $K_4$ of nonnegative $4 \times 4$ real matrices where entries sum to $4$. The uniform matrix for this dimension is denoted as $U_4$. The Dittert functional is represented by $\phi$.
Approach
The proof of the Dittert conjecture in dimension 4 was achieved by demonstrating the inequality $\frac{61}{32}-\phi(A)\geq \frac{1}{52}\lVert A-U_4\rVert_F^2$ for every matrix $A$ within the simplex $K_4$. This inequality implies that $\phi(A)$ is maximized when $\lVert A-U_4\rVert_F^2 = 0$, which occurs only when $A = U_4$.
The core of the proof involved reducing the problem to certifying the nonnegativity of a structured quartic polynomial. This polynomial contains sixteen variables and is defined on a simplex. To establish its nonnegativity, an exact rational constrained sum-of-squares (SOS) certificate was constructed.
The construction of this SOS certificate utilized an agent-guided symbolic-numeric procedure. This procedure integrated two main techniques: template selection and sequential rational recovery. The main SOS certificate comprised $152$ positively weighted rational squares. Additionally, $136$ smaller SOS blocks were constructed, each consisting of $16$ such squares.
Positivity within the certificate was confirmed through exact $LDL^{\mathsf{T}}$ decompositions. The complete polynomial identity was verified by exact coefficient comparison performed over the rational numbers ($\mathbb{Q}$). The resulting exact certificate underwent formal verification using the Lean proof assistant.
Findings
- The Dittert conjecture holds for dimension 4.
- For any matrix $A \in K_4$, the inequality $\frac{61}{32}-\phi(A)\geq \frac{1}{52}\lVert A-U_4\rVert_F^2$ is satisfied.
- Consequently, the uniform matrix $U_4$ is the unique maximizer of the Dittert functional $\phi$ on $K_4$.
- The proof relied on certifying the nonnegativity of a structured quartic polynomial in sixteen variables on a simplex.
- An exact rational constrained sum-of-squares certificate was constructed using an agent-guided symbolic-numeric procedure, incorporating template selection and sequential rational recovery.
- The main SOS certificate consisted of $152$ positively weighted rational squares, and $136$ smaller SOS blocks each consisted of $16$ such squares.
- Exact $LDL^{\mathsf{T}}$ decompositions confirmed positivity, and exact coefficient comparison over $\mathbb{Q}$ verified the polynomial identity.
- The exact certificate was formally verified using the Lean proof assistant.