Two right triangles inside every suspect

The Pythagorean classification turns a⁴ + b⁴ = c² into chains of smaller squares.

Start with a concrete example

With m=3,n=2, the three numbers m²−n²,2mn,m²+n² are 5,12,13, and 25+144=169. This is a concrete use of the right-triangle parametrization.

A small check: try the idea

Think with the concrete example above. You can try again.

For m=3,n=2, what does m²−n² equal?

Read the answer and reasoning

5. Compute 9−4=5. Squaring the difference instead would give (3−2)²=1, which is a different expression.

Build the idea in three steps

The core theorem not_minimal assumes a minimal suspect that is tidy enough — a odd, c positive — and derives False: death by too much structure.
First structure: a ^ 4 + b ^ 4 = c ^ 2 means (a ^ 2) ^ 2 + (b ^ 2) ^ 2 = c ^ 2, a Pythagorean triple. The coprime classification produces m and n with a ^ 2 = m ^ 2 - n ^ 2, b ^ 2 = 2 * m * n and c = m ^ 2 + n ^ 2.
The comments say what the reader should hear: from a ^ 2 = m ^ 2 - n ^ 2 once again a = r ^ 2 - s ^ 2, n = 2 * r * s, m = r ^ 2 + s ^ 2 — the same classification applied to the smaller triple it just made.

A small example

A familiar triple: 3² + 4² = 5². Then m = 3, n = 2 gives m ^ 2 - n ^ 2 = 5, 2 * m * n = 12, m ^ 2 + n ^ 2 = 13, and indeed 5² + 12² = 13². Every coprime triple arises this way, with one leg odd.

Use in Lean · original excerpt

Mathlib · db584cd · Four.lean

154theorem not_minimal {a b c : ℤ} (h : Minimal a b c) (ha2 : a % 2 = 1) (hc : 0 < c) : False := by155  -- Use the fact that a ^ 2, b ^ 2, c form a pythagorean triple to obtain m and n such that156  -- a ^ 2 = m ^ 2 - n ^ 2, b ^ 2 = 2 * m * n and c = m ^ 2 + n ^ 2157  -- first the formula:158  have ht : PythagoreanTriple (a ^ 2) (b ^ 2) c := by159    delta PythagoreanTriple160    linear_combination h.1.2.2161  -- coprime requirement:162  have h2 : Int.gcd (a ^ 2) (b ^ 2) = 1 :=163    Int.isCoprime_iff_gcd_eq_one.mp (coprime_of_minimal h).pow164  -- in order to reduce the possibilities we get from the classification of pythagorean triples165  -- it helps if we know the parity of a ^ 2 (and the sign of c):166  have ha22 : a ^ 2 % 2 = 1 := by167    rw [sq, Int.mul_emod, ha2]168    decide169  obtain ⟨m, n, ht1, ht2, ht3, ht4, ht5, ht6⟩ := ht.coprime_classification' h2 ha22 hc170  -- Now a, n, m form a pythagorean triple and so we can obtain r and s such that171  -- a = r ^ 2 - s ^ 2, n = 2 * r * s and m = r ^ 2 + s ^ 2172  -- formula:173  have htt : PythagoreanTriple a n m := by174    delta PythagoreanTriple175    linear_combination ht1176  -- a and n are coprime, because a ^ 2 = m ^ 2 - n ^ 2 and m and n are coprime.177  have h3 : Int.gcd a n = 1 := by178    apply Int.isCoprime_iff_gcd_eq_one.mp179    apply @IsCoprime.of_mul_left_left _ _ _ a180    rw [← sq, ht1, (by ring : m ^ 2 - n ^ 2 = m ^ 2 + -n * n)]181    exact (Int.isCoprime_iff_gcd_eq_one.mpr ht4).pow_left.add_mul_right_left (-n)

How to read this Lean

ht builds the triple from the equation itself — linear_combination shuffles the target equation into the triple’s shape, pure algebra bookkeeping. The classification receives three prepared facts: coprime legs (the pow of the neighboring coprime_of_minimal), the odd leg (ha22), and a positive hypotenuse. Deeper in this same theorem, the second triple a, n, m is classified again — nested structure, exactly what the descent consumes.

Original source ↗ · L154–181 Open the complete saved source

Where this idea is used

7. The veterans’ cabinet

Two right triangles inside every suspect

Start with a concrete example

A small check: try the idea

Build the idea in three steps

A small example

Use in Lean · original excerpt

How to read this Lean

Where this idea is used

Mika’s help desk

One thing at a time

In simpler words

A small clue