Four-colour Rado numbers for a(x-y)=bz: two new values and formally checked certificates

For a linear equation E and an integer k ≥ 1, the k-colour Rado number R_k(E) is the least n such that every k-colouring of {1, ..., n} contains a monochromatic solution of E. Using SAT solving we determine two cells that were empty in the table of four-colour values of Chang, De Loera and Wesley (ISSAC 2022): R_4(4(x−y)=3z) = 313 and R_4(5(x−y)=2z) = 625 = 5^4. The second is the first case with b ≥ 2 in which the four-colour number of a(x−y)=bz (a ≥ b+2, gcd(a,b) = 1) equals the general lower bound a^4, in analogy with their three-colour theorem R_3(a(x−y)=bz) = a^3. We also confirm R_4(2(x−y)=3z) = 226, listed as "> 225" in that table and recently announced in an unrefereed preprint by T. Ichikawa, and we recompute R_4(3(x−y)=2z) = 103 and R_4(x+y+c=z) for 1 ≤ c ≤ 12, in agreement with the literature. Every lower bound is certified by an explicit colouring checked by an independent brute-force program. Every upper bound is an unsatisfiability claim whose LRAT proofs, produced by CaDiCaL 2.1.3, are checked by the formally verified checker cake_lpr; for the largest instances we use cube-and-conquer, with the completeness of the cube split itself checked by cake_lpr. For 226, 313 and 625 the upper bounds were in addition verified for formulas without any symmetry-breaking clauses. Files: rado4.pdf is the note (9 pages). rado4_data.zip contains the colourings and an independent checker, the CNF generator, the formulas for a(x−y)=bz with SHA-256 checksums of all formulas, the cube files, the cube-and-conquer driver and the per-check logs of all cake_lpr runs. The LRAT proofs are not included because of their size. Not peer reviewed. The search code, the computations and a first draft of the note were produced with the help of an AI assistant (Claude, Anthropic). The author is responsible for the content.