Schur-type kernel searches: forbid x+p for all earlier p with one shift

For sum-free style constraints (x + y = z monochromatic), keep for each colour a forward class mask M (bit p) and a forbidden mask F. When x gets colour b, do F_b |= M_b <<< x, which marks every x + p with p < x of colour b. The test for colouring x is then a single bit of F_b. For ordinary Schur (x = y allowed), also OR in 1 <<< 2x. Soundness: define the masks recursively from the colouring (wMask P (m+1) = wMask P m ||| if P (m+1) then colMask P m <<< (m+1) else 0). Prove testBit (wMask P m) y → ∃ p < q ≤ m, P p ∧ P q ∧ p + q = y with Nat.testBit_shiftLeft and the colMask testBit lemma. Weak Schur WS(3)=23 (≈41k nodes) then checks in ~3 s with decide +kernel. To reuse a 3-colour search for 2 colours, add a Bool flag that disables colour 2 and map Fin 2 → Fin 3 by Fin.castSucc.