MATH.12:5.1 - Recover the witness in an arithmetic argument

For integers a,b, a proof shows that (a+b)^2-(a-b)^2 is divisible by four. The receiver wants the quotient.

Expanding the squares gives:

(a+b)^2-(a-b)^2 = 4*a*b.

The existence statement is “there is an integer k such that the difference is 4k.” Its witness-introducing step chooses k=a*b. The extracted operation is therefore multiplication of the two inputs, with the displayed identity as its justification.

At a=3,b=2, the difference is 25-1=24 and the operation returns k=6. The receiver can use 6 without reconstructing the expansion on every input.

Now ask for divisibility by eight. The old proof supplies 4ab, which is insufficient: at a=b=1 the difference is 4. A supplied stronger premise a=2r repairs the construction:

4*a*b = 8*r*b.

The new witness is r*b. If the input already carries r, the procedure uses it. If only an assertion that a is even is supplied, obtain the integer r with a=2r or use an available integer-division operation with its conditions. The changed proof identifies both the new premise and the additional input needed by its expression.