On a conjecture of Sun on sums of four numbers x(5x±1)/2

Z.-W. Sun conjectured (arXiv:2411.14308, Conjecture 5.5) that every integer n > 51 can be written as w(5w−1)/2 + x(5x−1)/2 + y(5y+1)/2 + z(5z+1)/2 with w, x, y, z natural numbers. We prove the stronger statement that every natural number n except n = 1 and n = 19 has such a representation. The problem reduces to finding lattice points on a sphere in a coset of 10Z⁴ with exactly two negative coordinates. We detect these with a degree-8 polynomial weight, and bound the resulting theta series of weights 2 to 10 and level 400 through explicit newform decompositions and Deligne's bound. This leaves 8,167,125 explicit integers below 10¹⁰, which are checked directly. The proof is computer-assisted: the decompositions are certified in ball arithmetic and the polynomial inequality in exact arithmetic. An independent audit by a separate AI run recomputed every step with different code and found no error. All modular-forms constants were also re-derived independently in SageMath, without PARI/GP, and every constant matched. An external review by ChatGPT found no objection to the main proof; its wording points have been corrected. No human expert has yet checked the argument. The mathematics, code and audits were produced by the AI system Claude (Anthropic) under the author's direction; see Section 8 of the paper. This record contains the paper, all programs, certificates, logs and the audit report.