CMP.8:4.5 - Derive refinement and stopping from the receiving requirement

Choose a stage from an a priori bound or use an observable enclosure with a justification that refinement reduces it. Include the work and storage needed to reach that stage. A bound polynomial in a numeric magnitude can still be exponential in that magnitude’s encoded length.

Identify what currently limits the answer: approximation loss, arithmetic, insufficiently known input, or an unresolved subject assumption. Refine the responsible part. Comparing two resolutions can reveal failure or help estimate a rate, but their agreement alone is not a bound on the unresolved remainder.

Stop when the supported result is sufficient or when further refinement is not worth its expected effect. C.11.DUA helps compare additional computation with acting under the remaining uncertainty. Return a conditional or partial answer when that is what the available construction supports.