funlean.
Step 22 / 64

High school

Tidy triangles share no factor

Primitive triples have coprime legs — and a recipe: m² − n² and 2mn.

Start with a concrete example

The triple 6,8,10 is twice 3,4,5. Dividing out a common factor gives a smaller basic triple. The formulas m²−n², 2mn, m²+n² produce 5,12,13 when m=3,n=2.

A small check: try the idea

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

How is 6,8,10 related to 3,4,5?

Read the answer and reasoning

Every entry is twice as large. 6=2×3, 8=2×4, 10=2×5. Dividing out a common scale gives the basic triple.

Build the idea in three steps

  1. A triple is primitive when its legs share no common factor: (3, 4, 5) is primitive, (6, 8, 10) is not — divide everything by 2 first, and what remains is the tidy original.
  2. The recipe IsPrimitiveClassified: every primitive triple is m ^ 2 - n ^ 2 and 2 * m * n for coprime m and n. The gear setting m = 3, n = 2 produces (5, 12, 13).
  3. The last field even certifies the parities with remainders on the two-clock: m % 2 = 0 with n % 2 = 1, or the other way round. One leg even, one leg odd — that certified pattern is exactly the lever the exponent-four descent pulls.

A small example

Two gear settings: m = 3, n = 2 gives 3 ^ 2 - 2 ^ 2 = 5 and 2 × 3 × 2 = 12 — the triple (5, 12, 13). And m = 5, n = 4 gives 9 and 40: 9 ^ 2 + 40 ^ 2 = 81 + 1600 = 1681 = 41 ^ 2.

Lean definition · original excerpt

Mathlib · db584cd · PythagoreanTriples.lean

/-- A primitive Pythagorean triple `x, y, z` is a Pythagorean triple with `x` and `y` coprime.Such a triple is “primitively classified” if there exist coprime integers `m, n` such that either* `x = m ^ 2 - n ^ 2` and `y = 2 * m * n`, or* `x = 2 * m * n` and `y = m ^ 2 - n ^ 2`.-/@[nolint unusedArguments]def IsPrimitiveClassified (_ : PythagoreanTriple x y z) :=  ∃ m n : ℤ,    (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧      Int.gcd m n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)

How to read this Lean

IsPrimitiveClassified asserts the existence of coprime integer parameters m and n with opposite parity, allowing the two legs to be exchanged. It does not claim uniqueness: (m,n) and (−m,−n) give the same two expressions. The exponent-four descent uses the classification twice, first for (a ^ 2, b ^ 2, c) and then for (a, n, m). Four.lean applies coprime_classification' from this file with the required sign and parity conditions.

Original source ↗ · L96–105Open the complete saved source

Where this idea is used

7. The veterans’ cabinet
I’m lost · Help

Mika’s help desk

Tidy triangles share no factor

One thing at a time

Read the three explanation steps first. The Lean source is there for a closer look afterwards; you do not have to read it first.

In simpler words

Primitive triples have coprime legs — and a recipe: m² − n² and 2mn.

Earlier ideas are listed under “Start with these ideas” on this page.

A small clue

Two gear settings: m = 3, n = 2 gives 3 ^ 2 - 2 ^ 2 = 5 and 2 × 3 × 2 = 12 — the triple (5, 12, 13). And m = 5, n = 4 gives 9 and 40: 9 ^ 2 + 40 ^ 2 = 81 + 1600 = 1681 = 41 ^ 2.

Close this panel to return to the exact place you were reading. These are prepared hints for this page.

Start with the first small story →