Certifying Failed Lean Proof-Agent Searches with Exact Replay

Large language models can propose Lean tactics (proof steps that Lean accepts or rejects), but a failed proof search is rarely actionable for a mathematical agent: did it search the proposed tactics poorly, miss a key tactic, or attempt an out-of-reach goal? We make one part of this diagnosis exact. At each reached Lean state we save the tactics the model proposed -- its *recorded support* -- and replay only those saved tactics under fixed depth and timeout bounds. Replay returns a Lean-checked proof, a *closed certificate* that no saved tactic path proves the goal within those bounds, or a timeout transcript. The closed certificate is the useful signal: it shows that replaying the same tactics cannot help, so any repair must add new candidates. We evaluate on CSLib-Holes, a frozen suite of 100 mechanically selected proof holes from the public CSLib Lean project, with the original proofs hidden from the agent. Base BFS-Prover replay solves 10/100 and leaves 74 closed certificates. Adding the statements of in-scope lemmas to the prompt repairs 16/74, against 6/74 for a matched search-only widening, and iterating these Lean-checked additions raises the oracle-free solved count from 10/100 to 39/100, every repair re-checked by Lean. A target-statement control repairs 12/74, so whether the failed-search frontier (the goals left unproved at the dead ends of the failed search) helps beyond the target statement is directional rather than decisive (pooled exact McNemar $p=0.227$). This is a bounded audit layer for proof agents.