Failure Signals Are Control State: Resource-Aware Retry Scheduling for Lean Agents

Verifier feedback is usually treated as text to place in the next prompt. We study a different role: feedback as control state for deciding which failed theorem deserves another draw, how much budget it receives, and when to stop. We implement a minimal fixed-policy agent harness whose replay reproduces every recorded action, stop, budget, and accounting decision; a fault-injection suite triggers the intended monitor on 7/7 corruptions. The most robust intervention is also the simplest: suppressing retries after verifier timeout saves 10.8% and 11.3% of retry tokens in two seed blocks while preserving solve parity under all 24 draw orderings. Under the pre-specified ordering, the full frozen rules reach uniform's held-out solve count with 27.5% and 33.9% fewer retry tokens; ordering medians are 17.8% and 32.1%, while a fitted dynamic allocator adds no consistent benefit. Including the common 202-theorem first-stage screen, the measured pipeline saves 11.7% and 17.0% of completion tokens and avoids 24 and 33 model calls at the same total verified count. The first block's theorem-bootstrap interval crosses zero; the second excludes it. We then ask why selective control matters. An exact, hash-matched timing replay of 536 recovery branches finds that prompt prefill is only 0.99% of model-serving time. A four-slot continuous-batching check strengthens rather than reverses this result. Capped generations, however, are 25.0% of branches but consume 38.0% of total measured phase time and never reach Lean. The unchanged rules save 26.7% and 44.2% at equal solve count on two Kimina blocks, but produce the predicted exact null on a DeepSeek cohort without timeout or truncation roots. A prospective intervention that uniformly splits the same nominal 12,288-token budget finds no detectable yield gain and consumes more realized compute. A fourth study re-tests a targeted 8,192-token cap on three new disjoint seed blocks over the same 40 held-out roots, under a specification frozen before any branch was staged: it leaves the verified set unchanged on every root in every block while saving 9.8–11.4% of completion tokens and 11.2–13.3% of directly measured GPU energy, a cost result that its frozen specification anticipated as such.