feat: Add Unconditional Odlyzko Bound problem

[bixbyr]

feat: Add unconditional Odlyzko Bound problem. This gives an explicit numerical lower bound to the discriminant of a number field. The proof requires non-trivial complex analysis.

Co-authored-by: Gemini 3.1 Pro gemini@google.com

[kim-em]

🤖 Claude says:

The statement isn't Odlyzko's theorem, and I don't think it's true. Odlyzko's bound is asymptotic: |d_K|^(1/n) ≥ 60.8^(r₁/n) · 22.3^(2r₂/n) − ε(n) with ε(n) → 0. Collapsing that into a single constant c independent of K says root discriminant ≥ 22.3 · e^(−c/n), which demands ε(n) = O(1/n). That needs c ≥ n · log(22.3 / m(n)) where m(n) is the minimal root discriminant in degree n, and the known minima are well below 22.3 for large n (degree 8 is about 5.8), so the required c grows without bound. Small cases don't refute it — ℚ only forces c ≥ log 60.8 — which is what makes it look plausible.

Two faithful repairs. Either add a degree hypothesis, as the FLT project's axiom does:

axiom Odlyzko_statement (K : Type*) [Field K] [NumberField K]
  [NumberField.IsTotallyComplex K] (hdim : Module.finrank ℚ K ≥ 18) :
  |(NumberField.discr K : ℤ)| ≥ 8.25 ^ Module.finrank ℚ K

or state the ε-form directly: ∀ ε > 0, ∃ n₀, ∀ K, n₀ ≤ finrank ℚ K → ….

Also drop the LeanEval.lean import line (same as on #475) and the trailing whitespace in the docstring.

[alreadydone]

This is equivalent to

Suggested change

	theorem odlyzko_bound_unconditional :
	∃ (c : ℝ), 0 < c ∧
	∀ (K : Type*) [Field K] [NumberField K],
	let r1 := (InfinitePlace.nrRealPlaces K : ℝ)
	let r2 := (InfinitePlace.nrComplexPlaces K : ℝ)
	((discr K).natAbs : ℝ) ≥ (60.8 : ℝ) ^ r1 * (22.3 : ℝ) ^ (2 * r2) * Real.exp (-c) := by
	theorem odlyzko_bound_unconditional :
	∃ (c : ℝ), c < 1 ∧
	∀ (K : Type*) [Field K] [NumberField K],
	let r1 := (InfinitePlace.nrRealPlaces K : ℝ)
	let r2 := (InfinitePlace.nrComplexPlaces K : ℝ)
	((discr K).natAbs : ℝ) ≥ (60.8 : ℝ) ^ r1 * (22.3 : ℝ) ^ (2 * r2) * c := by

and I think it's better to use Real.eulerMascheroniConstant and Real.pi in the bases of the exponentiation.

(formula from ImperialCollegeLondon/FLT#458 (comment))