Persistent failure of quartic SOS exactness

An explicit rational cubic in 14 variables has sphere maximum one but a strictly larger degree-four moment value. The resulting quartically regularized polynomial fails sum-of-squares exactness for every positive regularization parameter, with its quadratic and cubic data fixed.

For the 25-term cubic specified in Proof.md, set

With

the actual global minimum is , attained at . The polynomial is nonnegative and is not a sum of squares of real polynomials. Every SOS lower bound satisfies

At the origin the gradient vanishes and the Hessian is . The complete minimizer set is also classified: an isolated axis point and an eight-dimensional sphere. The specialization answers the stationary, non-PSD-Hessian question in Cartis–Zhu, Remark 2.3, for the Euclidean quartic regularizer.

A unique nondegenerate minimizer

A second fixed cubic, still with 25 monomials in 14 variables, is

Replacing by preserves the same radius and minimum . The unique global minimizer is , and its Hessian is positive definite, with diagonal blocks

Nevertheless, the exact minimum shift is not SOS for any positive regularization parameter. Every SOS lower bound obeys

The companion proof reuses the same rational moment certificate. Positive curvature here is at the minimizer; the Hessian at the stationary origin remains .

Reading

The independent statement interface is PersistentSOSChallenge.lean; the proof entry is PersistentSOSSolution.lean.

Reproduction

lake build
python3 scripts/check_certificate.py
python3 scripts/independent_certificate_check.py --negative-controls
python3 scripts/check_unique_minimizer.py
python3 scripts/check_sources.py
python3 scripts/audit_axioms.py

The formal statements, verification commands and exact-commit evidence are recorded in VERIFICATION.md. Submission and registration are separate steps. No optimal SOS value, smallest possible dimension, worldwide priority, or human specialist review is claimed.

MIT license, copyright 2026 JD Jones.