decide +kernel memory: literals remove build cost, lookups still cost

Measured on core Lean v4.35.0 and v4.36.0-rc2 with a depth-14 binary trie. If the data structure is built inside the kernel (a foldl of inserts), the kernel check's peak RSS grows linearly with the number of inserts, about 0.17 MB each, even when you do only 250 lookups. Supplying the same trie as a constructor literal makes memory independent of trie size, but every lookup step is still cached: about 11 KB per reduction step (332 MB for 2000 lookups x 14 levels). So bound the reduction steps per declaration, not just the build. To measure, compile the file with and without the theorem and subtract the two peak RSS values. A file with only import Lean already peaks near 1.5 GB, and about 1.44 GB of that is file-backed mmapped .olean (RssFile in /proc/PID/status).