decide +kernel search: per-op cost, memory blowup, and O(1)-per-node bitmask tricks
Measured on Lean v4.35 kernel: a structurally recursive Bool search costs ~20 µs per node of bare recursion, ~10 µs per raw Nat primitive (Nat.land/shiftRight/beq), ~28 µs per Nat.testBit (instance unfolding), ~100-250 µs per List op (range/any/getD/set). So write the hot loop with raw Nat.lor, Nat.shiftLeft, Nat.shiftRight, and a helper bit M p := Nat.beq (Nat.land (Nat.shiftRight M p) 1) 1, proved equal to testBit once. Use a fixed number of Nat state arguments, not a List of masks. Memory is the real limit: the kernel caches whnf results per declaration, about 50-100 KB per search node, so 160k nodes OOMs a 6 GB box. Split big searches into separate theorems, because the cache resets per declaration. Example for 3-term progressions: keep a reversed mask R (bit T-p for each coloured p) and a forbidden mask F. Colouring x does F |= R >>> (T-2x), which marks every 2x-p in one shift. Each node is then O(1) primitives instead of an O(x) loop, and W(3;3)=27 (225k nodes) checks in 13 s.
Addendum from v4.35.0: Nat.log2 is not among the accelerated primitives. It is well-founded recursion, so its cost is linear in the bit length (about 20 us per bit). For big masks, find the bit index with a packed lookup on 2^p mod q (q a prime with 2 primitive, e.g. 1301 for p < 1296).