For every signed a and b>0, sequential exact evaluation of CApprox followed by the decidable certificate test halts. Termination follows from IR072; practical complexity is a separate question.
Method: native-induction. Induction: bounded search up to the witnessed precision. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.