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)\geq \frac{1}{52}\lVert A-U_4\rVert_F^2$ for every $A\in K_4$. Consequently, $U_4$ is the unique maximizer of $φ$ on $K_4$. 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 $LDL^{\mathsf{T}}$ decompositions certify positivity, and exact coefficient comparison over $\mathbb{Q}$ verifies the complete polynomial identity. The resulting exact certificate is formally verified using the Lean proof assistant.