diff --git a/verification/lean-guard b/verification/lean-guard
index 54e1ace..5f03315 100755
--- a/verification/lean-guard
+++ b/verification/lean-guard
@@ -94,6 +94,7 @@ if [ "$AVAIL_MB" -lt "$MIN_FREE_MB" ]; then
     exit 1
 fi
 
+
 # ── Guard 3b: global-headroom clamp (2026-07-03 swap-pressure incident) ─────
 # A cap is a PROMISE of memory to lean; never promise more than the machine
 # can afford right now. Requested caps that exceed (available − floor) are
@@ -101,11 +102,14 @@ fi
 # into swap even when lean itself stays within its cap. Clamp, don't fail:
 # most compiles peak far below their cap (measure before raising — the
 # incident's 9G scopes served a file whose true peak was 753MB).
+REQ_MEM_MB=$MEM_MB
+WAS_CLAMPED=0
 MAX_AFFORD_MB=$(( AVAIL_MB - MIN_FREE_MB ))
 if [ "$MEM_MB" -gt "$MAX_AFFORD_MB" ]; then
     echo "lean-guard: clamping -M ${MEM_MB} -> ${MAX_AFFORD_MB}MB (avail=${AVAIL_MB}MB, floor=${MIN_FREE_MB}MB)"
     MEM_MB=$MAX_AFFORD_MB
     CGROUP_MB=$(( MEM_MB + 1024 ))
+    WAS_CLAMPED=1
 fi
 if [ "$MEM_MB" -lt 1024 ]; then
     echo "FATAL: headroom clamp would leave lean < 1024MB — machine too loaded to compile safely"
@@ -120,19 +124,56 @@ run_leancmd() {
       timeout --signal=TERM --kill-after=15 "$TIMEOUT_SEC" \
       lean -M "$MEM_MB" -o "$OLEAN_FILE" "$LEAN_FILE" "$@"
 }
-if systemd-run --user --scope -p MemoryMax=10M --quiet -- /bin/true 2>/dev/null; then
-    # --scope runs the command as a child of THIS shell (env inherited),
-    # merely placing it in a fresh cgroup with the hard caps below.
-    systemd-run --user --scope --quiet \
-        -p MemoryMax="${CGROUP_MB}M" -p MemorySwapMax=256M \
-        -- taskset -c "$CORES" \
-           timeout --signal=TERM --kill-after=15 "$TIMEOUT_SEC" \
-           lean -M "$MEM_MB" -o "$OLEAN_FILE" "$LEAN_FILE" "$@"
-    EXIT_CODE=$?
-else
-    echo "  (systemd-run unavailable — falling back to lean -M only)" >> "$LOG_FILE"
-    run_leancmd "$@"
-    EXIT_CODE=$?
+do_compile() {
+    if systemd-run --user --scope -p MemoryMax=10M --quiet -- /bin/true 2>/dev/null; then
+        # --scope runs the command as a child of THIS shell (env inherited),
+        # merely placing it in a fresh cgroup with the hard caps below.
+        systemd-run --user --scope --quiet \
+            -p MemoryMax="${CGROUP_MB}M" -p MemorySwapMax=256M \
+            -- taskset -c "$CORES" \
+               timeout --signal=TERM --kill-after=15 "$TIMEOUT_SEC" \
+               lean -M "$MEM_MB" -o "$OLEAN_FILE" "$LEAN_FILE" "$@"
+    else
+        echo "  (systemd-run unavailable — falling back to lean -M only)" >> "$LOG_FILE"
+        run_leancmd "$@"
+    fi
+}
+do_compile "$@"
+EXIT_CODE=$?
+
+# ── Guard 3a: lazy wait-and-retry after a clamped memory abort (pass 3) ─────
+# The clamp above protects the host, but under ambient memory pressure it
+# can cut a KNOWN-NEEDED cap (ReduceSpec peaks ~6.5G) and guarantee an
+# interpreter abort that reads like a proof regression. Lazy semantics keep
+# light files free: only when a CLAMPED run dies on memory (134 abort /
+# 137 cgroup kill) and LEAN_MEM_WAIT_SEC>0, wait — still under the
+# single-flight lock — until the ORIGINAL request is affordable, then retry
+# once at full cap. Default 0: behavior unchanged.
+MEM_WAIT_SEC=${LEAN_MEM_WAIT_SEC:-0}
+if [ "$WAS_CLAMPED" -eq 1 ] && [ "$MEM_WAIT_SEC" -gt 0 ]; then
+    WAITED=0
+    # Retry ladder: whenever headroom improves MATERIALLY (>= +1536MB over
+    # the cap that just died, or reaches the full request), retry at the
+    # new clamp. The full request may never be affordable on a loaded host
+    # even though the true peak is — climbing the ladder finds the passing
+    # clamp without knowing the peak. Monotone caps + deadline => bounded.
+    while { [ "$EXIT_CODE" -eq 134 ] || [ "$EXIT_CODE" -eq 137 ]; } \
+          && [ "$WAITED" -lt "$MEM_WAIT_SEC" ] && [ "$MEM_MB" -lt "$REQ_MEM_MB" ]; do
+        sleep 20; WAITED=$(( WAITED + 20 ))
+        AVAIL_MB=$(free -m | awk '/Mem:/{print $7}')
+        NEW_AFFORD=$(( AVAIL_MB - MIN_FREE_MB ))
+        if [ "$NEW_AFFORD" -ge "$REQ_MEM_MB" ] || [ "$NEW_AFFORD" -ge $(( MEM_MB + 1536 )) ]; then
+            MEM_MB=$(( NEW_AFFORD < REQ_MEM_MB ? NEW_AFFORD : REQ_MEM_MB ))
+            CGROUP_MB=$(( MEM_MB + 1024 ))
+            echo "lean-guard: clamped run died (rc=$EXIT_CODE); retrying at -M ${MEM_MB}MB after ${WAITED}s (avail=${AVAIL_MB}MB, request=${REQ_MEM_MB}MB)"
+            echo "[$(date -u +%F' '%T)] RETRY $LEAN_FILE (M=${MEM_MB}MB cg=${CGROUP_MB}MB avail=${AVAIL_MB}MB after ${WAITED}s)" >> "$LOG_FILE"
+            do_compile "$@"
+            EXIT_CODE=$?
+        fi
+    done
+    if [ "$EXIT_CODE" -eq 134 ] || [ "$EXIT_CODE" -eq 137 ]; then
+        echo "lean-guard: memory-death persists after ${WAITED}s of ladder retries (last -M ${MEM_MB}MB, request ${REQ_MEM_MB}MB) — keeping the failure"
+    fi
 fi
 
 case $EXIT_CODE in