MATH.12:5 - Archetypal Grounding

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.

MATH.12:5.2 - Read a function equivalence as two transformations

Suppose f maps each a in A to a pair in B×C. A proof can split this into two functions by projecting its output:

Split(f) = (a ↦ first(f(a)), a ↦ second(f(a))).

Conversely, given g:A→B and h:A→C, pair their values:

Join(g,h) = a ↦ (g(a),h(a)).

Applying Join after Split gives, at each a:

(first(f(a)),second(f(a))) = f(a).

Applying Split after Join returns g and h pointwise. Thus the argument supplies transformations in both directions, together with the equalities that justify using the returned functions.

For f(n)=(n+1,n^2), Split gives g(n)=n+1 and h(n)=n^2. Joining their values at n=3 returns (4,9). The projections and applications are the computational content of the proof.

The equality concerns functions with values determined by their input. If evaluating f is expensive, the expression using two calls can repeat work; calculate f(a) once and keep its pair when both components are needed.

If the proposed implementation instead reads and increments a hidden counter, repeated calls change the situation. A single call returning (c,c) might give (1,1), while separate component calls yield (1,2). This no longer implements the fixed mathematical f used by the proof. Include the changing state in the model and reconsider the transformation before using this function equivalence to reorganize the work.

MATH.12:5.3 - Extract a case decision and its answer

For a rational input r=p/q, with integer p and positive integer q, construct either an indication that r=0 or a rational y such that r*y=1.

The proof examines the decidable integer condition p=0:

• If p=0, return Zero with the equality r=0.
• Otherwise return Inverse(q/p). Since p is nonzero, the fraction is defined, and (p/q)*(q/p)=1.

The result includes which case holds. At p=4,q=6 it returns Inverse(3/2). At p=0,q=5 it returns Zero. This tag lets a receiving calculation choose its continuation.

Merely reporting that one of the two conclusions holds loses the branch information the continuation needs. The construction obtains that information by testing an integer, then carries it with the result.

Now replace the rational representation by access to successively narrower rational intervals enclosing an arbitrary real number. The rational procedure’s test p=0 is no longer available. A nondegenerate rational interval containing zero does not by itself establish that the represented real is zero, because it also contains nonzero values. An interval [0,0] would establish equality, but the representation does not guarantee reaching such an interval. The previous proof does not supply a terminating zero test for this representation.

The next move is to obtain an appropriate decision procedure under additional input conditions, change the requested output to allow an unresolved case, or retain the existence conclusion without claiming the obtaining operation. The rational construction remains usable on its stated inputs.