CMP.2:4.5 - Establish the result and expose its computational cost

Use the base and smaller-call assumptions to establish the returned property. Recombination must work for every smaller answer allowed by its specification, including the selected tie behavior. When deriving a program from an existing proof, MATH.12 recovers the operations hidden in that proof.

Count the subcalls and local work. A recurrence for mathematical values and a recurrence for computational cost answer different questions. For balanced segment splitting with interval views, constant-cost arithmetic and the four-value join, the work satisfies W(n)=W(floor(n/2))+W(ceil(n/2))+O(1), giving O(n) operations. Sequential depth-first evaluation retains O(log n) summaries on its call stack. Copying each subarray instead adds work at each level; growing integer values also change the cost per addition.

If equal subproblems recur, CMP.3 can identify and share them. If the decomposition generates alternatives that can be ruled out, CMP.4 can construct those exclusions. If representation dominates the cost, compare the access and update operations before replacing the mathematical construction.