funlean.
Step 17 / 64

University

Pick the smallest solution

Rank the hypothetical solutions by how often λ divides c: one must be smallest.

Start with a concrete example

If a set of positive whole-number badges has any members, one badge has the smallest number. Choosing that badge gives a precise target: producing a still smaller valid badge would be impossible.

A small check: try the idea

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

Among hypothetical badge sizes 10,6,9, which is smallest?

Read the answer and reasoning

6. Smallest refers to size, not reading order. Finding an even smaller allowed candidate would contradict minimality.

Build the idea in three steps

  1. A Solution’ is a hypothetical generalized solution bundled as one object: the numbers a, b, c, the unit u, the λ-divisibility conditions, the coprimality, and the equation H stored as a field.
  2. A Solution is the same tuple with one extra line: λ ^ 2 ∣ a + b. Neighboring lemmas of this file send any Solution’ to a Solution with the same multiplicities.
  3. Rank hypothetical solutions by the natural-number multiplicity of λ in c. If at least one solution exists, Solution.exists_minimal selects one of least rank. It does not assert that a solution exists without that assumption.

A small example

Rank the suspects by their record: among all hypothetical solutions, choose one whose λ-count in c is smallest. If the story can always produce a strictly smaller count, the smallest record cannot exist at all.

Lean definition · original excerpt

Mathlib · db584cd · Three.lean

/-- We say that `S : Solution` is minimal if for all `S₁ : Solution`, the multiplicity of `λ` in`S.c` is less or equal than the multiplicity in `S₁.c`. -/def Solution.isMinimal : Prop := ∀ (S₁ : Solution hζ), S.multiplicity ≤ S₁.multiplicity omit [NumberField K] [IsCyclotomicExtension {3} ℚ K] ininclude S in/-- If there is a solution then there is a minimal one. -/lemma Solution.exists_minimal : ∃ (S₁ : Solution hζ), S₁.isMinimal := by

How to read this Lean

The definition is the gauge: compare solutions by the multiplicity of λ inside c, and call the one with the smallest such number minimal. The two directive lines before the lemma trim ambient typeclass assumptions and bind S explicitly — the statement needs only the structure fields. Below the excerpt, the proof body collects every solution’s multiplicity into a nonempty family of natural numbers and reads off its least element.

Original source ↗ · L226–233Open the complete saved source

Where this idea is used

2. The case of three7. The veterans’ cabinet
I’m lost · Help

Mika’s help desk

Pick the smallest solution

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

Rank the hypothetical solutions by how often λ divides c: one must be smallest.

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

A small clue

Rank the suspects by their record: among all hypothetical solutions, choose one whose λ-count in c is smallest. If the story can always produce a strictly smaller count, the smallest record cannot exist at all.

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 →