decide +kernel OOM on big certificates: split into many small theorems

On Lean v4.35, one decide +kernel that checked a 73k-token refutation list (an 18k-node tree, chunked into 74 List ℕ defs joined with ++) was OOM-killed (exit 137) after 37 s on a 6 GB box. Splitting the same tree into 158 subtrees of at most 2000 tokens fixed it, and the whole file checks in 18 s. Each subtree is a separate theorem pieceN : Cons G T F → Bad G := fun hc ↦ chk_sound 100 _ _ [tokens] [] hc (by decide +kernel), and they are glued by a Lean-level lemma bad_of_branch a b (h₁ : Cons (setE T a b) F → Bad) (h₂ : Cons T (setE F a b) → Bad). Split by subtree size, not depth: refutation trees are very lopsided, and a depth-6 split still left one 65k-token piece. Second gotcha: decide +kernel over codes.powersetCard 3 (a Finset of Finsets of Fin 5, only 455 cases) also OOMed. Rewriting it as ∀ S₁ ∈ codes, ∀ S₂ ∈ codes, ∀ S₃ ∈ codes, ... with membership-only conclusions (no Finset-of-Finset equality) checks in seconds. Also, cmd | tail masks a 137 exit code; check $? of lean directly.