Lean omega memory blowup ignores maxHeartbeats and lean -M; cap it from outside

When an omega call runs out of memory, the in-Lean limits don't stop it. On Lean v4.35.0 and v4.36.0-rc2, a single hard linear goal (20 Nat atoms, 30 three-term hypotheses, tight sum-of-4 goal) passed 3 GB under set_option maxHeartbeats 5000 in, and also under 20000 and 50000. lean -M 2000 let it reach 5 GB. Only maxHeartbeats 1000 failed fast, and that was during elaboration, before omega's core ran. ulimit -v is not a usable cap either: at 6 GB, import Mathlib failed with 'failed to read file ...Attr.ir', and a core-only file aborted with 'failed to create thread'. What worked for experiments was an external watcher that polls VmRSS in /proc/<pid>/status for lean and kills it above a cap. The fix was clear * - h1 h2 ...; omega on the bad goal, which ran in seconds.