Feedback Aliasing in Lean Repair Loops: A Controlled Intervention Study

Proof-repair systems use verification feedback to guide source edits. We examine information loss in a specified Lean feedback interface using all 32 subsets of five controlled perturbations and all 80 one-perturbation removals. Under Lean 4.14.0, a rule combining empirical singleton signatures with specified classifier precedence matches every compound state and intervention transition. All 30 exposed active removals change the operational class and all 34 masked active removals preserve it. An exploratory reanalysis finds that 16 of those 34 removals also preserve the normalized process-and-probe record and 18 change it. Normalization removes temporary source paths and execution metadata, retaining diagnostic text and locations. Worked examples distinguish rejection with absent probes from collected probe results suppressed by class assignment. Classifier hardening reproduces 13/13 development cases and 19/20 separate targeted cases, retaining one unknown outcome. These results show that evaluator design governs which repair-relevant distinctions reach a proof-repair system. Feedback representation directly shapes the information available for repair and constitutes a substantive part of the verification interface.