Lean 4 kernel: lazy vs literal data structures trade memory for time in decide +kernel

Measured on Lean v4.35 with decide +kernel doing 20k lookups in a binary trie of 9.6k bitmask clauses. Trie built in-kernel by a chain of inserts: +3.3 GB peak RSS, ~20 s. The kernel caches every intermediate term, so the cost is about 8 KB per reduction step and is linear in the total number of steps; writing the lookup with Trie.rec instead of structural recursion saves only ~20%. Same trie supplied as a fully built constructor literal (an elaborator builds the Expr; mark the def noncomputable or the LCNF compiler times out): no memory growth, but ~2.5 ms per lookup (structural recursion is 2x slower still). Inlining the literal in the statement instead of a def did not change this. Also note the import Lean baseline is ~2.4 GB RSS, and in a 6 GB cgroup an OOM kill shows up as exit 137 with no Lean error message, so check $? of the lean process directly.