
Re: Formal Proof Language Example  HumanReadable?
Posted:
Jun 27, 2009 11:09 PM


Andrew Tomazos wrote: > Isn't q just the GCD of (c + a) and (c  a) ? > > It's clear that b*b = (c+a) * (ca). > > It is also clear that the exponents of the prime factorization of > (b*b) must all be even. > > I am not sure how you conclude from this that ((c+a)/q) and ((ca)/q) > must be perfect squares? Can you express this step formally?
If we let p1, ..., pn be the prime factorization of b, then we obviously have that b*b = p1^2 * ... * pn^2. Since b*b = (c+a) * (ca), it obviously stands (c+a) and (ca) each get some subset of these prime factors.
For each factor p_i^2, it stands to reason that there are three ways it can end up in the product (c+a) * (ca). It can be a factor of only (c+a), a factor of only (ca), or p_i could be a factor of each.
The GCD q will be made up only of the p_i^2 factors that were split between the two quantities; if we divide q from both of the quantities, we are therefore left with the product of numerous perfect squares, which must itself be a perfect square.
Another way to think about it is to look at the exponents of prime factors of b*b, c + a, and c  a. Since b*b's prime factorization must have all even exponents, the corresponding prime must have either both odd or both even exponents in c + a and c  a. If you divide those quantities by their GCD, you will either be subtracting even exponents by an even exponent (producing an even) or odd exponents by an odd exponent (producing an even), leaving you with only even exponents.
 Beware of bugs in the above code; I have only proved it correct, not tried it.  Donald E. Knuth

