Julin S (May 15 2022 at 20:13): Julin S (May 15 2022 at 20:13):I had been reading the first page of the foreword of 'The seventeen provers of the world' at https://www.cs.ru.nl/~freek/comparison/comparison.pdf
There a 'geometrical proof' (is that a correct term?) for the irrationality of √2 is mentioned.
Screenshot-from-2022-05-16-01-41-03.png
Call the original triangle ABC, with the right angle at C. Let the hypothenuse AB = p, and let the legs AC = BC = q. As remarked, p² = 2q².
Reflect ABC around AC obtaining the congruent copy ADC. On AB position E so that BE = q. Thus AE = p − q. On CD position F so that BF = p. Thus DF = 2q − p. The triangle BF E is congruent to the original triangle ABC. EF is perpendicular to AB, the lines EF and AD are parallel.
Now, position G on AD so that AG = EF = q. Since AEF G is a rectangle, we find AG = q. Thus, DG = F G = AE = p − q. So, the triangle DF G is an isosceles right triangle with a leg = p − q and hypothenuse = 2q − p.
If there were commensurability of p and q, we could find an example with integer lengths of sides and with the perimeter p + 2q a minimum. But we just constructed another example with a smaller perimeter p, where the sides are also obviously integers. Thus, assuming commensurability leads to a contradiction.
I got everything mentioned there except what's mentioned at the end.
Where it is mentioned that the minimum perimeter of a triangle should be p+2q but a triangle of lesser perimeter (p) has been constructed.
But the lesser perimeter triangle has different sides.
Why would that mean p and q are not commensurable?
Could anyone help me understand this?
Li-yao (May 15 2022 at 21:16):p^2 = 2q^2 has rational solutions iff it has integer solutions. Assume there is an integer solution (p,q), i.e., an isoceles right triangle with hypothenuse p and leg q. Then that construction finds a smaller integer solution (2q-p, p-q). Iterating it, we get an infinite sequence of right triangles with decreasing integer perimeters, which contradicts the well-foundedness of N.
Julin S (May 16 2022 at 04:32):Oh.. Now I'm beginning to see it.
(p, q) could be made into (2q-p, p-q). So we can keep going and keep making an infinite number of similar triangles.
But what did the author mean by saying something about the lower limit of the perimeter of triangle being at least p+2q though?
It went on to say that a triangle with a lower perimeter (p) could be made because of which p/q is not rational.
Li-yao (May 16 2022 at 04:47):I think it's phrased a bit awkwardly, but it's the other way of laying out the infinite descent argument: assume those triangles with integer sides exist, let (p,q) be the triangle such that its perimeter (p+2q) is the smallest. Then we construct another triangle with a smaller perimeter p. That contradicts the assumption that the previous one was the smallest.
Li-yao (May 16 2022 at 04:48):So I'm guessing "... with the perimeter p+2q a minimum" is really saying "we choose (p,q) such that p+2q is the smallest perimeter".
Julin S (May 16 2022 at 05:08):I just thought of something else.
Does just having a 'transformation' from (p, q) to (2q-p, p-q) necessarily mean that it will go on forever (assuming it stops before it starts generating negative values)?
Because for example, Euclid's gcd algorithm 'transforms' (p, q) to (q, p mod q) where it stops when q is zero.
In the case of gcd(8,3),
(8,3) -> (3,2) -> (2,1) -> (1,0)
and it stops there.
Should having the (p, q) to (2q-p, p-q) transformation mandate an infinite sequence?
Li-yao (May 16 2022 at 05:14):Yes, the argument is that if you could find an isoceles right triangle with integer sides (p,q), then the operation could be repeated ad infinitum from there.
Li-yao (May 16 2022 at 05:17):p,q > 0 and p^2 = 2q^2 implies that (2q-p,p-q) are two positive numbers (the lengths of the smaller triangle in the drawing)
Julin S (May 16 2022 at 05:40):Thanks! I think I get it.
If a right isosceles triangle with hypotenuse p and leg q exists, where p and q are positive integers (ℕ₁), then we can say that
p = √2q
p² = 2q²
If we can have a such a triangle, we can also make a right isosceles triangle with hypotenuse (2q-p) and leg (p-q).
2q - p
= 2q - √2q
= √2(√2 - 1)q
√2(√2 - 1) > 0 and q > 0.
So,
√2(√2 - 1)q > 0
ie, 2q - p > 0
Likewise,
p - q
= √2q - q
= (√2 - 1)q
(√2 - 1) > 0 and q > 0.
So,
(√2 - 1)q > 0
ie, p - q > 0
And now, we can keep using the new values to generate smaller values.
I suppose we say 'by induction' or something here.
Something like that, right?
Julin S (May 16 2022 at 05:44):Could there be a way to prove things like this in coq? Could geocoq be a way?
Li-yao (May 16 2022 at 05:46):Yeah, you construct an infinite descending sequence of positive integers, and you can use induction to prove that there is no such sequence.
Li-yao (May 16 2022 at 05:48):Geometry gives an intuition for the construction but it can be carried out completely symbolically (as you just did in fact). Knowing arithmetic is sufficient to do it in Coq.
Li-yao (May 16 2022 at 05:56):You do need a bit of creativity to make the proof only talk about nat (so √2 can't even be mentioned), but it's quite feasible.
Julin S (May 16 2022 at 06:17):Yeah, that's what I was thinking . I had heard that mentioning non-nat numbers (ie, float I guess) could complicate proofs quite fast. :sweat_smile:
Julin S (May 16 2022 at 06:17):Thanks!
Notification Bot (May 16 2022 at 06:17):Julin S has marked this topic as resolved.
Last updated: Dec 05 2023 at 12:01 UTC