P0: Lean/leanchecker must not overload lambda — narrow Mathlib imports, lake build vs leanchecker tiers, thread cap, no heavy kernel decide

[noahgift]

Operator, verbatim, 2026-09-25: "yes to all, p0" (answering the cop's 4 proposals below). Context, verbatim: "remember this host must be able to do other work, so never let it get overloaded"

Measured 2026-09-25 07:34Z on lambda:

• leanchecker ProvableContracts (pvl-a, PID 614236) used 51 threads, about 9 cores, and 58 to 60 GB RSS.
• Host load was 79 on 48 cores; memory was 99 of 125 GB.
• Cause: the project does require mathlib (5.4 GB of compiled .olean files). leanchecker reloads and re-checks the whole imported environment. Our own 237 .lean files are a small share of that.

P0 — all four:

1. Narrow the imports: no import Mathlib. Import only the specific Mathlib modules each file needs. Receipt: RSS and wall time before and after.
2. Split the check tiers:
   • Day to day: lake build, which trusts Mathlib's compiled files and checks only our files.
   • Release gate only: leanchecker, run under systemd-run --user --scope -p MemoryMax=24G -p CPUQuota=800%, or on gx10 after checking disk space.
   • The pv discharge check --leanchecker call sites and CI must follow this split.
3. Cap threads: at most 8 threads for Lean and leanchecker (-j8 / LEAN_NUM_THREADS=8 or its equivalent). Make it the default in the pv wrapper.
4. Keep computation out of the kernel: for PVL: prove all 7 escape-allowlist axioms (DPO x3, f16 bound, NF4 x3) instead of confirming them #4347 (the NF4 table and the others), prefer norm_num, simp or rfl lemmas over heavy decide. Never use native_decide, because it adds an axiom.

Done when: a full pv discharge check --leanchecker runs within 24G and 800% CPU on lambda, and a regression guard fails if an unscoped leanchecker invocation appears in scripts or CI.

[noahgift]

Already implemented on B3 (fold/b3-contracts-ont-docs, PR #4317): c2efb7f, 0a79b45 (the caps are ceilings: can be lowered, never raised) and 1498cf9 (guard self-exclusion), folded at 41488ee.
All four asks are covered, per c2efb7f:

• Narrowed imports, no bare import Mathlib.
• pv discharge check --leanchecker and run default to LEAN_NUM_THREADS=8 inside a systemd-run --scope --slice=agent.slice -p MemoryMax=24G -p CPUQuota=800% scope.
• build.sh runs lake build with 8 threads.
• NF4 decide +kernel was measured light (2.15 s, 2.7 GB); native_decide is not used.

Guard: scripts/check_leanchecker_scoped.sh (a 23-row case table).
Done-when receipt: full-tree pv discharge check --leanchecker exits 0 in 162 s, with scope memory peak at the 24G cap and at most 11 threads. Before: 51 threads, 58–71 GB.
Closes when #4317 lands. It carries no Fixes #4348.