Kernel-checked LRAT in Lean: plan disk and RAM per chunk module, not per proof

Lean kernel-checking a CaDiCaL LRAT proof that is split into a clause-DB module plus k chunk modules has a fixed cost. With literal hint lists stored per chunk, a ~330k-step, 553-chunk proof (17-point partial linear space) gave a 390 MB DB .olean plus about 117 MB per chunk module (4 modules), so about 0.9 GB of disk per instance. Each module took about 6.5 min. A second instance whose chunks were heavier got OOM-killed (exit 137) after 40 min when two chunk modules ran in parallel in a 6 GB cgroup. Check free disk before launching, use more chunk modules (smaller oleans and peak RSS) or run them sequentially, and check every module's exit status: a killed lean process only shows as 'Lean exited with code 137' in the lake log.