Try
Find the greatest common divisor of 48 and 18 without using a division-with-remainder step. Both numbers are even. Dividing both by two changes the gcd, so record the removed factor outside the pair: gcd(48,18)=2·gcd(24,9). Now 24 is even and 9 is odd. Halving 24 alone preserves the remaining gcd. Repeating that guarded operation reaches the pair (3,9).
Predict the next move. Both coordinates are odd, so subtract the smaller from the larger: (3,9) becomes (3,6). Halve the even coordinate, giving (3,3). Subtract equal values, giving (0,3). The remaining gcd is 3, and the removed factor is 2, so the original answer is 6. Check directly that 6 divides both original inputs. That check alone does not prove it is the greatest common divisor; the invariant below supplies the missing argument.
We use nonnegative integer inputs A and B, not both zero. The state is (s,u,v), initially (1,A,B). The number s is an external scale, always a positive power of two. The coordinates u and v are the current reduced problem. A zero coordinate is a stopping condition, not an invitation to keep halving zero.
Predict
A tempting rule says “halving an even input never changes the gcd.” Test it on (12,8): the gcd is 4, but halving just 12 gives (6,8), whose gcd is 2. The other coordinate’s parity matters. By contrast, gcd(12,5)=gcd(6,5)=1. Explain the difference in terms of factors of two shared by the two coordinates.
The rules are deliberately ordered. First stop if either coordinate is zero. Otherwise, if both are even, halve both and double s. If exactly one is even, halve that one and keep s. If both are odd, subtract the smaller from the larger and keep s; when equal, subtract the second from the first. We count subtraction and subsequent halving as separate transitions. A more compressed implementation might combine them, but it would have a different trace convention.
Predict whether s must decrease to prove termination. It need not: s can increase. Instead watch the positive integer u+v. Every nonterminal move decreases that sum, even when s doubles.
Experiment
Complete the following worked trace and annotate the reason for every move. The table records the state after each transition; the first row is the initial state.
| Scale s | u | v | Potential u+v | Reason for this state |
|---|
| 1 | 48 | 18 | 66 | Initial inputs |
| 2 | 24 | 9 | 33 | Both even: extract a common factor of two |
| 2 | 12 | 9 | 21 | Only u is even |
| 2 | 6 | 9 | 15 | Only u is even |
| 2 | 3 | 9 | 12 | Only u is even |
| 2 | 3 | 6 | 9 | Both odd: subtract u from v |
| 2 | 3 | 3 | 6 | Only v is even |
| 2 | 0 | 3 | 3 | Equal odd coordinates: subtract and stop |
Change the initial inputs to (40,14). Write a complete trace before opening the feedback. Then try (0,14). Do not copy the first trace’s scale or run an update after a stopping condition.
Check the changed cases
The states for (40,14) are (1,40,14), (2,20,7), (2,10,7), (2,5,7), (2,5,2), (2,5,1), (2,4,1), (2,2,1), (2,1,1), (2,0,1). The answer is 2. For (0,14), stop in the initial state and return 14. These examples test guard ordering as well as arithmetic. The pair (0,0) is excluded from this lesson’s contract; it has no greatest positive common divisor under the definition being used.
Understand
The invariant is gcd(A,B)=s·gcd(u,v). It holds initially because s=1 and the current pair is the original pair. We must prove that every permitted transition preserves it.
Only one coordinate is even. Suppose u=2a and v is odd. Every common divisor of a and v divides 2a and v. Conversely, if d divides 2a and v, then d is odd because v is odd. Write 2a=kd. As d is odd and the product is even, k must be even. Therefore d divides a. The two pairs have exactly the same positive common divisors, proving gcd(2a,v)=gcd(a,v). The argument works with the coordinates reversed too. The false unconditional-halving rule omitted the oddness used here.
Both coordinates are even. We need gcd(2a,2b)=2gcd(a,b). One independent justification uses the earlier Euclidean/Bézout theorem: if g=gcd(a,b), then integers h,k satisfy ha+kb=g. The number 2g divides 2a and 2b, and any common divisor of those numbers divides h(2a)+k(2b)=2g. Hence their gcd is 2g. This relies on a theorem already proved by the Euclidean algorithm, not on the binary algorithm now being established. Halving both coordinates and doubling s therefore preserves the displayed invariant. In this branch both coordinates are positive because the stopping test came first.
Odd subtraction. For u≥v>0, a positive integer divides both u and v exactly when it divides both u−v and v. The forward direction subtracts; the reverse direction adds v back. Thus gcd(u,v)=gcd(u−v,v). Oddness is not necessary for this identity, but it identifies the branch where the binary rules have not already chosen halving. The difference of two odd coordinates is even, possibly zero. A zero result stops on the next guard check.
Termination. A nonterminal state has two positive integer coordinates. Common halving divides their sum by two. Single-coordinate halving reduces it by half that positive coordinate. Subtraction reduces it by the positive smaller coordinate. In every case u+v strictly decreases, stays a positive integer, and neither update produces two zeros. There cannot be an infinite strictly decreasing sequence of positive integers. Indeed there are at most A+B−1 transitions under these rules. That numerical bound is a termination bound, not a claim of efficiency in the number of input bits.
At termination one coordinate is zero and the other, say d, is positive. Its gcd with zero is d. The invariant now gives gcd(A,B)=s·d, exactly the returned answer. The proof combines invariant preservation, state validity, termination and the stopping condition; none alone establishes the whole algorithm’s correctness.
Apply
Suppose a proposed implementation adds an optional swap of u and v. Swapping preserves the gcd and the external scale, but it does not decrease u+v. Repeatedly swapping (3,5) and (5,3) gives an infinite computation with a perfectly preserved invariant. Repair the rule before claiming termination.
One repair allows at most one swap immediately followed by a mandatory decreasing move, before any further swap can occur. Treat that pair of elementary actions as a macro-step. Every macro-step strictly decreases u+v and has at most two elementary actions. Terminal states stop before either action. This supplies a termination argument for the repaired procedure. An invariant cannot rule out arbitrary motion among states with the same value.
For positive inputs, the initial common halvings extract exactly the smaller of their two powers-of-two exponents. For example, 24=8·3 and 40=8·5 share three such halvings, leaving scale 8 and odd pair (3,5). Further odd subtraction and single-coordinate halving preserve that scale. Zero requires separate handling: every power of two divides zero, so it has no largest finite exponent under that definition.
What this proof does not establish
A positive-integer potential proves termination. It does not by itself prove a logarithmic iteration bound, constant-time integer arithmetic, or a particular bit complexity. Large inputs have more bits, and each operation has an implementation cost. Likewise, the current state records the gcd but not coefficients expressing it as a combination of A and B. Tracking and repairing those coefficients is additional work in the extended algorithm.
Continue
Return to the Euclidean algorithm and Bézout proof if the common-divisor or linear-combination arguments need a refresher. Here the new mechanism is guarded parity reduction with an external scale. In practice, explain why each branch is enabled, show the invariant’s value, and prove a decrease before concluding that a changed procedure terminates.
The next extension will track integer coefficient certificates through halving as well as subtraction. Keep that task distinct from returning the correct gcd: a claimed coefficient pair must be checked against the original inputs, including the scale removed at the start.
