Four-colour Rado numbers of a(x-y)=bz: seven values with checked proofs

Let R_k(a,b) be the least n such that every k-colouring of {1,...,n} has a monochromatic solution of a(x-y)=bz (gcd(a,b)=1). We determine seven four-colour values: R_4=461, 741 and 1501 for 3(x-y)=4z, 5(x-y)=4z and 6(x-y)=5z, R_4=313 for 4(x-y)=3z, R_4=625 for 5(x-y)=2z and for 5(x-y)=3z, and R_4=2001 for x-y=5z, none of which we found in the literature. The lower bounds are explicit colourings, each from a construction that works for every number of colours; the upper bounds are SAT computations on a small subset of {1,...,n} split by cube-and-conquer, with every proof checked by the formally verified checker cake_lpr. We prove R_k(a(x-y)=(a-1)z) >= a^k+a^(k-1)-2a+1 for all k,a>=2; equality holds for k=4 and a=3,4,5,6, but fails for k=5 and a=3,4 (R_5(4(x-y)=3z) >= 1401 > 1273). We also collect lower bounds and evidence on a conjectured recursion R_4=b(R_3+2a)+1 for a<b. Version 2 adds the four values 313, 625, 625, 2001 with checked proofs, a block construction for x-y=bz, and the five-colour bounds. Not peer reviewed. Developed with the help of an AI assistant (Claude, Anthropic); the author is responsible for the content.