MATH.12:1 - Problem frame

Use this pattern when a mathematical proof says that an object can be obtained, but you still need the operation that obtains it. The proof may describe the object through several intermediate results, hide it inside a pair, or use cases whose choice must be made from the input.

Recover the values and operations carried by the argument. A proof that a number is divisible by four can supply the quotient; a proof connecting two function types can supply transformations between their functions. When a step supplies only existence, the same reading identifies the construction still needed.

First useful move: find where the wanted object is introduced. Write the expression for that object and the inputs used to form it. Follow each needed input back to a supplied value, an available operation or a missing construction.

The reader needs functions, pairs, case distinctions and elementary mathematical reasoning. The arithmetic cases use integers and fractions. The function case explains its own notation. Use an already available operation directly when it returns the required object. An existence conclusion can be sufficient when the receiving question does not require obtaining a witness.

This method works through constructive proof steps and their computation rules. A claim about every input needs a construction that can be applied to every input in that scope. Some proofs establish their conclusion without supplying such a construction; :4.4 determines what can still be used from them.