Sun's 1–3–4 Conjecture: A Computer-Assisted Proof for OEIS A335624

We prove the conjecture of Sun associated with OEIS A335624 by a computer-assisted argument. The nonnegative integers that have no representation $n=x^2+y^2+z^2+w^2$ with nonnegative integral coordinates and $x+3y+4z$ a square are exactly $16^ke$, where $k\geq0$ and $e\in\{8,24,40,344\}$. Building on the quaternionic framework of Machiavelo--Tsopanidis and Sun's sign criterion, the proof combines a norm-$26$ transfer controlled modulo $3$ with a positivity refinement for even norms. It establishes existence for $n\geq17\,000\,000\,000$ with $16\nmid n$. The remaining interval is verified by three algorithmically distinct implementations: two bitmap sieves and a scalar search that tests each integer separately. All three find only the four base exceptions. We provide an alternative modular verification of the representation lemma, source code, certificates, execution records, and a constructive procedure for obtaining representations.