If direct perturbation fails its bounded pilot, separately implement negative translation plus Friedman A-translation on a tiny supported arithmetic proof calculus. Test induction, binders and eigenvariables; emit ordinary HA certificates. No Markov axiom or automatic arbitrary Lean import.
Method: certificate-reconstruction. Induction: none. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.