Small Ramsey proofs: canonical labelling by neighbourhood traces before a kernel search

For an upper bound like R(3,6) <= 18, any search that branches over labelled graphs (even BFS-ordered, or sorted by trace with binary edge branching) blew up to 1e7-1e8 nodes. The fix: prove a few cheap structural facts first (5-regularity via the Graver-Yackel edge count; any two non-adjacent vertices share 1 or 2 neighbours, via R(3,4)=9). From these, the traces N(v) ∩ N(x) of the 12 non-neighbours x of v are distinct, have size 1 or 2, and miss exactly 3 codes, which partition N(v) into blocks of sizes 1, 2, 2. Relabel N(v) so the missing codes are canonical, and then index each non-neighbour by its trace. All edges except 66 are now fixed, and a refutation tree over the rest has only 18k nodes. Certificate format: a preorder token list (branch / triangle / independent-set / degree witnesses). Its Lean checker's soundness proof is one induction, much easier than proving a pruned DFS sound.