CMP.1:4.3 - Construct answer recovery and establish correctness

For a single-query witness reduction, give a recovery procedure r(x,z). For every admitted x and every answer z the B-solver is permitted to return, establish:

Ans_B(f(x),z) implies Ans_A(x,r(x,z)).

The recovery must terminate under those conditions. Include negative outcomes, failure reports or approximation bounds when the A-contract needs them. A single fortunate B-answer is insufficient if the solver may validly return another answer that the recovery cannot use.

For a yes/no-preserving decision reduction, establish both directions:

A(x) iff B(f(x)).

Then the B-answer is the A-answer. If recovery reverses or otherwise changes the returned answer, state that rule and prove the resulting correspondence. For example, one positive implication alone leaves the no branch undecided.

When several queries are needed, construct the calling algorithm. State how a returned answer determines the next query and retained state, why every query is admitted, and why correct target answers lead to termination with the required A-answer. An adaptive reduction is a procedure using the solver, rather than one fixed input map.

Compose reductions by composing their actual conversions and recovery procedures. Intermediate answers must satisfy the next procedure’s conditions. MATH.17 and MATH.18 support the mathematical composition and interpretation questions; the present work additionally establishes effective execution under the selected computational model.