MATH.22:4.4 - Trace the consequences that the receiving work uses

For each required result, locate the affected proof step.

• Retain a proof when its steps use only assumptions that remain.
• Try another proof when the old one uses the removed assumption. A dependency of one proof need not be a necessary premise of the theorem.
• Keep a conditional result when the receiving use can supply the additional premise.
• Return a countermodel when the conclusion fails under the revised assumptions.
• Leave a particular consequence unresolved when neither an argument nor a countermodel has been obtained.

Apply the same reasoning to constructions. Check whether their inputs are still admitted, the operations remain defined, and the properties used by the next step still follow. For example, :5.1 retains cancellation after dropping commutativity but loses unrestricted rearrangement of factors.

When a proof is formalized, its recorded dependencies can help find affected steps. They report what that proof uses. A claim that no proof can avoid an axiom requires an additional argument.

If the result will generate data or a program, trace what the new principle supplies operationally. An existence argument and an effective construction support different next uses. MATH.12 handles extraction; the relevant computational method handles execution and cost.