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?

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.

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.

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.

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".

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?

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.

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)

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?

Could there be a way to prove things like this in coq? Could geocoq be a way?

Yeah, you construct an infinite descending sequence of positive integers, and you can use induction to prove that there is no such sequence.

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.

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.

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:

Thanks!

Julin S has marked this topic as resolved.

Last updated: Dec 05 2023 at 12:01 UTC