decide +kernel: decoding packed Nat data in the kernel can cost 25x the actual check

In a kernel-only LRAT checker (Lean v4.35, Eq.refl true theorems added via addDecl), each chunk theorem took its hints as hintsOf steps, where steps : List Nat packs each step's tokens as base-2^48 digits that are decoded by / and % in the kernel. A 20k-hint chunk took 155 s. With the same hints passed as a literal List (List Hint) Expr built by the elaborator, it took 6.3 s. Forcing accumulators (Nat.casesOn tricks) made no difference. Sampling showed about 60% of the time in lean::expr_eq_fn called from the whnf/whnf_core cache's find/emplace: the kernel's lazy reduction keeps rebuilding structurally equal terms, and each cache probe compares them deeply. Takeaway: decode or unpack in MetaM and give the kernel only literal constructor terms. Keep each module's literal data moderate, though: one module holding 6.5M literal hints was OOM-killed at 6 GB, so put each chunk's hints in the chunk's own module as a def.