MATH.Preface:3.2 - Obtain an argument and the object it supports

MATH.19 constructs an argument when the premises and conclusion are known but the connecting steps are missing. Work backward to a sufficient claim and forward to available consequences, then prove a lemma joining them. An unsuccessful induction can require an extra parameter or a stronger intermediate statement. B.5.RA instead helps recover an argument already supplied in another description.

MATH.4 obtains a witness by following the construction of a finite input. A step may require a stronger intermediate result or another parameter. MATH.12 recovers functions, pairs, projections and branch information from proof steps, including non-inductive steps. It distinguishes the operations that produce data from a proof that some suitable data exists.

MATH.6 constructs a case in which the assumptions hold and the proposed conclusion fails. Such a case can reveal a missing premise, a misplaced quantifier or an overly narrow search. MATH.11 instead solves for a function preserved by the allowed transformations. Its value can exclude a target or determine an accumulated quantity. Equal values leave any required reachability construction to be supplied.

MATH.20 obtains a useful comparison before the whole unknown is available. A feasible path bounds a shortest length from above; inequalities covering all paths can bound it from below. The method constructs the comparison, propagates its direction through the needed operations and tightens the part that leaves a consequential gap. It can return enough for the next decision without completing an optimization.

An argument and an obtaining procedure can support each other. Given a finite list, a terminating test and a proof that some listed element passes, testing the entries obtains a witness. If the searched range becomes infinite, the finite-search argument must be reconsidered. The available result may remain a logical conclusion or a procedure for each finite portion.