Odlyzko.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

1 declarations, 0 contain sorry, 1 declared as axioms

Bounds for root discriminants of number fields

Let K be a number field of degree n over the rationals. Minkowski gave a lower bound (depending only on n) for the absolute value of the discriminant of K. Using this bound he was able to deduce that every number field other than the rationals was ramified at at least one prime.

In the proof of FLT being formalized, we need stronger bounds which do not follow from Minkowski's elementary argument. By analysing the behaviour of the zeros of the zeta function of K, Odlyzko was able to give such stronger bounds. These bounds were improved by Poitou in his 1977 paper "Sur les petits discriminants". Equation 26 of the paper implies the below bound, and an explicit reference for it is the table on p17 of the paper (in fact 8.25 can be beefed up to 9.3, but we do not need this).

Why do we need this?

The original proof by Wiles and Taylor-Wiles of FLT contains a crucial step where they "switch to the prime 3", and apply the Langlands--Tunnell theorem to deduce that the 3-torsion in an elliptic curve over ℚ, if irreducible, is modular. In the argument we are formalizing, we switch to 3 at a different point. The advantage of this is that it avoids the Langlands-Tunnell theorem (which needs non-Galois cubic cyclic base change); the analysis we need is easier. We switch to 3 only after we have constructed a compatible family of Galois representations with conductor 2 from the Frey curve (using hard modularity lifting theorems), and we use this bound below to demonstrate that such a family cannot exist. The argument involves a careful analysis of the 3-torsion in the 3-adic specialization of the family; it is analogous to Fontaine's proof that there is no nontrivial abelian variety over ℤ.

References

[Georges Poitou, Sur les petits discriminants][poitou_odlyzko_bounds]

Currently available at https://www.numdam.org/item/SDPP_1976-1977__18_1_A6_0/

The github tracking issue for this assumption is #458 on the FLT github repository.

Imports (2)

Imported by 1 file

FLT.lean

axiom Odlyzko_statement An "Odlyzko bound" for the root discriminant of a totally complex number field of degree 18 and above line 58 source
Source documentation
An "Odlyzko bound" for the root discriminant of a totally complex number field of degree 18 and above.

extra axioms: Odlyzko_statement what this means
Statement uses: Field, NumberField, NumberField.IsTotallyComplex, GE.ge, Nat, Module.finrank, Rat, OfNat.ofNat, Real, abs, NumberField.discr, HPow.hPow, OfScientific.ofScientific, Bool.true
23 instances, coercions and auxiliary constants left out.
```
axiom Odlyzko_statement (K : Type*) [Field K] [NumberField K] [IsTotallyComplex K]
  (hdim : finrank ℚ K ≥ 18) : |(discr K : ℝ)| ≥ 8.25 ^ finrank ℚ K
```