When Verifier Feedback Hides Repair Progress: Compound Failures in Lean

Verifier-guided agents use compiler and proof-assistant feedback to choose subsequent edits. With several defects present, one diagnostic can reveal the earliest failure and hide progress on later defects. We measure this effect in Lean 4 through a complete factorial design over four error-inducing source edits and one context-sensitive control, covering 32 source states and all 80 single-edit removals. A precedence model matches all 32 observed states and all 80 repair transitions. The five-category diagnostic map contains 1.875 bits about a 5-bit edit state under the uniform factorial design, leaving 3.125 bits unresolved. The repair graph exposes a larger credit-assignment loss: 64 interventions remove an edit that fails in isolation; 30 change the diagnostic category, whereas 34 effective repairs—53.1% of active-edit removals—retain the same category as an earlier defect continues to dominate the feedback. A context-sensitive control adds 16 unchanged transitions through a separate mechanism, and a 5-step repair sequence exposes the hidden failures sequentially. These exact results establish diagnostic movement as a low-recall progress signal under compound failures. Verifier-guided evaluation can recover more state information from raw diagnostics and edit-conditioned verification trajectories alongside terminal correctness.