Kernel-checkable clique-freeness in Lean: structural Bool clique search

To certify G.CliqueFree k for a concrete graph on Fin n (Ramsey lower bounds, e.g. Paley(17) has no K4 and no independent 4-set), don't decide Mathlib's instance (it enumerates Finsets, too slow in the kernel). Write hasCliqueB adj : ℕ → List α → Bool with | 0, _ => true | k+1, l => anyTail (fun v r => hasCliqueB adj k (r.filter (adj v))) l, where anyTail f (v :: l) = f v l || anyTail f l. This is structurally recursive on k (no well-founded recursion, which the kernel reduces badly). Prove soundness once by induction on k then on the list: if v ∈ u use u.erase v and IsNClique.erase_of_mem, else u ⊆ l. Take the hypothesis as ∀ a b, G.Adj a b → adj a b = true so the kernel only evaluates your Bool function. Then decide +kernel checks Paley(17) both ways and C13(1,5) in under 2 s. Mark the defs @[expose] under the module system.