Lean 4: split a multi-hour kernel `decide`/rfl check across modules so lake parallelizes and checkpoints it

Problem: a proof by reflection consisting of hundreds of Eq.refl true theorems (here, chunks of an LRAT refutation checked against a big literal data structure) was generated inside one tactic run, so one lean process ran for hours with no parallelism, and if it was killed nothing was saved.

Fix (Lean v4.35.0): three metaprograms instead of one tactic. 1. A command in module DB.lean computes the data and adds it with addDecl as plain definitions: X.db (the literal), X.steps_j (one List Nat literal per chunk), plus X.info : List Nat describing the chunk boundaries. 2. A command chunks X k K in modules C_k.lean (each only import DB) reads X.info back by walking the List.cons literal of the definition value ((env.find? n) -> .defnInfo d -> d.value) and adds X.chunk_j : check X.db a_j X.steps_j = true for j % K = k. 3. A tactic in a module importing all C_k assembles the final proof term from the constants by name. After that, lake checks the C_k modules in parallel, and finished modules survive restarts as cached .olean files.

Measured: the imported 226 MB .olean is file-backed and mmapped, so it is shared between processes. Each chunk process used only 0.4-1.4 GB of anonymous memory, while the monolithic run needed a 3.5 GB peak. Two workers fit in a 6 GB cgroup; check /proc/PID/smaps_rollup (Anonymous vs Pss_File) rather than RSS, which counts the shared pages once per process.

Gotchas: never let two lake build invocations build the same module at once, so build the DB module first and then start the chunk modules. Keep Elab.async false around each addDecl of a theorem, or the kernel checks of one module run in parallel and their memory adds up.