The smaller suspect appears

m, r, s all become squares: i² = j⁴ + k⁴ with |i| < |c|. Contradiction.

Start with a concrete example

Suppose badge 50 was the smallest allowed badge. If the proof constructs an allowed badge smaller than 50, the assumption was impossible. The construction, not just saying “go lower”, is the work.

A small check: try the idea

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

If 50 is the smallest allowed size, what would an allowed size 40 imply?

Read the answer and reasoning

A contradiction with the chosen minimum. The comparison is 40<50. The crucial point is that 40 is still allowed, not just numerically smaller.

Build the idea in three steps

From the nested classification, the positive numbers m, r and s are forced to be perfect squares: m = i ^ 2, r = j ^ 2, s = k ^ 2 — positivity rules out the negative squares.
But m = r ^ 2 + s ^ 2, so i ^ 2 = j ^ 4 + k ^ 4: a brand-new Fermat42 solution, assembled purely from squares of the smaller numbers.
The gauge bites: m = i ^ 2 and c = m ^ 2 + n ^ 2 give |i| ≤ i ^ 2 = m < c = |c| under the established positivity conditions. The new solution is smaller, contradicting minimality, which requires |c| ≤ |i|.

A small example

Trace one spiral: if the smallest suspect had c = 50, the descent would hand back a solution whose |c| is below 50. The badge was already the smallest — so this cannot be.

Use in Lean · original excerpt

Mathlib · db584cd · Four.lean

239  -- from m = r ^ 2 + s ^ 2 we now get a new solution to a ^ 4 + b ^ 4 = c ^ 2:240  have hh : i ^ 2 = j ^ 4 + k ^ 4 := by grind241  have hn : n ≠ 0 := by grind242  -- and it has a smaller c: from c = m ^ 2 + n ^ 2 we see that m is smaller than c, and i ^ 2 = m.243  have hic : Int.natAbs i < Int.natAbs c := by244    apply Int.ofNat_lt.mp245    rw [← Int.eq_natAbs_of_nonneg (le_of_lt hc)]246    apply lt_of_le_of_lt (Int.natAbs_le_self_sq i)247    rw [← hi, ht3]248    apply lt_of_le_of_lt (Int.le_self_sq m)249    exact lt_add_of_pos_right (m ^ 2) (sq_pos_of_ne_zero hn)250  have hic' : Int.natAbs c ≤ Int.natAbs i := by251    apply h.2 j k i252    exact ⟨hj0, hk0, hh.symm⟩253  apply absurd (not_le_of_gt hic) (not_not.mpr hic')

How to read this Lean

The last lines are the point: hh assembles the new solution’s equation from j ^ 4 and k ^ 4; hic chains |i| ≤ i ^ 2 = m < m ^ 2 < m ^ 2 + n ^ 2 = c; hic' applies the minimality hypothesis h.2 at the triple (j, k, i). absurd then pairs a claim with its negation — no flourish, just arithmetic honesty. This is Fermat’s own stairway from the 17th century, still carrying weight.

Original source ↗ · L239–253 Open the complete saved source

Where this idea is used

7. The veterans’ cabinet

The smaller suspect appears

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