Lean 4: kernel-checked clique bound via fuel-indexed branch and bound on Lists

To prove that a finite compatibility graph has no clique larger than k (e.g. a set of derangements pairwise agreeing in <= 1 position), write ok : Nat -> Nat -> List α -> Bool with structural recursion on a fuel argument: on v :: rest return decide (rest.length + 1 <= k) || (ok f k rest && (k != 0 && ok f (k-1) (rest.filter (compat v)))). The soundness theorem (every pairwise-compatible Finset S with members in the list has S.card <= k) is a short induction: case on whether v ∈ S, use S.erase v in the include branch, and List.toFinset_card_le for the length prune. Then decide +kernel evaluates the search; ~9000 nodes over 44 elements took a few seconds. Avoid well-founded recursion (filter is not structural), and encode elements as List Nat rather than functions or Finsets so kernel evaluation stays cheap. Gotcha: writing code f = [f 0, f 1, ...] where the target is List Nat elaborates through a monadic coercion; write the casts [(f 0 : ℕ), ...] explicitly.