Construct t with 2^t>=12*K*S*J. Failure of the decidable test |b*u_t-a|>2*b*2^-t implies |c-z|<=3*2^-t<=epsilon, contradicting IR069. Decidability of this single finite rational test yields the certificate in HA; no Markov rule is used.
Method: native-order. Induction: none. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.