A stairway that must end

A gauge that always strictly decreases cannot decrease forever: Fermat’s descent.

Start with a concrete example

Start on stair 5 and move to a strictly lower nonnegative stair each time. You cannot do this forever. A descent proof shows that a supposed smallest counterexample would force another, smaller one.

A small check: try the idea

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

Can nonnegative whole-number stair heights strictly decrease forever?

Read the answer and reasoning

No. Starting at 5, there are only finitely many nonnegative heights below it. The proof must actually construct a smaller valid candidate.

Build the idea in three steps

Everything is staged: a minimal solution carries the smallest λ-gauge, and the earlier pages manufacture strictly smaller solutions from any solution.
The displayed proof is the final argument: from the minimal Smin, the descent lemma exists_Solution_multiplicity_lt produces Sfin with a strictly smaller multiplicity, via a round trip through a Solution’.
Finally linarith compares the two gauges: Sfin’s is smaller than Smin’s, yet Smin was chosen smallest. The contradiction closes Fermat’s case n = 3, the theorem FermatLastTheoremFor 3.

A small example

Any staircase of counts that strictly decreases at every step cannot descend forever — Fermat named this infinite descent. Here the count is the multiplicity of λ in c, and it lives among nonnegative integers, so there are only finitely many steps.

Use in Lean · original excerpt

Mathlib · db584cd · Three.lean

749/-- Fermat's Last Theorem for `n = 3`: if `a b c : ℕ` are all non-zero then750`a ^ 3 + b ^ 3 ≠ c ^ 3`. -/751public theorem fermatLastTheoremThree : FermatLastTheoremFor 3 := by752  let K := CyclotomicField 3 ℚ753  let hζ := IsCyclotomicExtension.zeta_spec 3 ℚ K754  have : NumberField K := IsCyclotomicExtension.numberField {3} ℚ _755  apply FermatLastTheoremForThree_of_FermatLastTheoremThreeGen hζ756  intro a b c u hc ha hb hcdvd coprime H757  let S' : FermatLastTheoremForThreeGen.Solution' hζ :=758  { a := a759    b := b760    c := c761    u := u762    ha := ha763    hb := hb764    hc := hc765    coprime := coprime766    hcdvd := hcdvd767    H := H }768  obtain ⟨S, -⟩ := FermatLastTheoremForThreeGen.exists_Solution_of_Solution' S'769  obtain ⟨Smin, hSmin⟩ := S.exists_minimal770  obtain ⟨Sfin, hSfin⟩ := Smin.exists_Solution_multiplicity_lt771  linarith [hSmin Sfin]

How to read this Lean

Read the proof slowly: the three obtain lines unpack the round trip — the minimal solution becomes a smaller one. The proof then feeds the minimality inequality hSmin Sfin into the arithmetic: linarith juxtaposes it with the strictly smaller count produced by the descent, and the only surviving conclusion is that no Sfin ever existed. The set_option line above the docstring just loosens an elaboration heuristic; it is not part of the mathematics.

Original source ↗ · L749–771 Open the complete saved source

Where this idea is used

2. The case of three

A stairway that must end

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