Explicit Littlewood lower bound $L(1,\chi)\ge0.0617/\log\log q$ under $\Re s>7/8$ zero-freeness

Proved

QRHLittlewood.littlewood_lower_explicit

by @bwdaugherty · 1 vote · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorynumber-theory

Let $q\ge10^{100}$ and let $\chi$ be a primitive real Dirichlet character modulo $q$ such that $L(s,\chi)\neq0$ for every complex $s$ with $\Re s>7/8$ . Then

L(1,\chi)\ \ge\ \frac{0.0617}{\log\log q}.

Through the class number formula this gives explicit lower bounds for class numbers of quadratic fields of large discriminant under the same hypothesis.

Formalization Note $L(1,\chi)$ is compared through its real part; for a real character it is a positive real number.

Preamble

import Mathlib.NumberTheory.Harmonic.EulerMascheroni
import Mathlib.NumberTheory.LSeries.DirichletContinuation

open Real

Formal statement

namespace QRHLittlewood

theorem littlewood_lower_explicit (q : ℕ) [NeZero q] (hq : (10 : ℝ) ^ 100 ≤ q)
    (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hreal : ∀ a : ZMod q, (χ a).im = 0)
    (hH : ∀ s : ℂ, 7 / 8 < s.re → DirichletCharacter.LFunction χ s ≠ 0) :
    (617 / 10000 : ℝ) / Real.log (Real.log q) ≤ (DirichletCharacter.LFunction χ 1).re := by sorry

end QRHLittlewood

Source

B. W. Daugherty, S. Ryan, G. Ward, Certified harmonic-measure barriers and explicit Littlewood bounds from zero-free regions, https://doi.org/10.5281/zenodo.23400116, Theorem 2(ii),

a=7/8

q_0=10^{100}

(constant

c_1=0.0617

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Statement. Let $q$ be a natural number with $q\neq 0$ and $10^{100}\le q$ (as real numbers). Let $\chi$ be a $\mathbb{C}$ -valued Dirichlet character modulo $q$ such that

$\chi$ is primitive (its conductor equals $q$ );
$\chi$ is real-valued: $\operatorname{Im}\chi(a)=0$ for all $a\in\mathbb{Z}/q\mathbb{Z}$ ;
$L(s,\chi)\neq 0$ for every complex $s$ with $\operatorname{Re}s>7/8$ .

Then

\frac{0.0617}{\log\log q}\;\le\;\operatorname{Re}L(1,\chi),

where $0.0617=617/10000$ exactly and $\log$ is the natural logarithm.

Here $L(s,\chi)$ is Mathlib's Dirichlet $L$ -function: the unique meromorphic continuation to all of $\mathbb{C}$ of $\sum_{n\ge1}\chi(n)n^{-s}$ (built from Hurwitz zeta functions); it is a total function $\mathbb{C}\to\mathbb{C}$ , and at a pole (only possible at $s=1$ for the trivial character) it returns a fixed finite junk value. "Primitive" means the conductor of $\chi$ (the least $d\mid q$ through which $\chi$ factors) equals $q$ . "Real-valued" means $\operatorname{Im}\chi(a)=0$ for every residue class $a\in\mathbb{Z}/q\mathbb{Z}$ , including non-units (where $\chi(a)=0$ anyway).

Edge cases.

Since $q\ge 10^{100}$ , $\log\log q\ge\log(100\log 10)\approx 5.44>0$ , so no junk values of $\log$ or of division occur on the left side.
Since $q\ge 3$ , primitivity excludes the trivial character, so $\chi$ is a primitive quadratic character and $L(s,\chi)$ is entire; the value at $s=1$ is a genuine value, not a pole junk value. For moduli $q$ admitting no primitive real character the statement is vacuous.
Hypothesis 3 is a conditional zero-free half-plane assumption on this particular $\chi$ (it includes $s=1$ and all $\operatorname{Re}s\ge1$ ). Nothing else about zeros is assumed.
The conclusion concerns only $\operatorname{Re}L(1,\chi)$ and is a one-sided (lower) bound with $\le$ .

Human review

Endorsed by Shuze Chen · Oct 16, 2026
Confirmed by the moderator at approval.
Endorsed by @bwdaugherty · Oct 16, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Explicit Littlewood lower bound L(1,χ)≥0.0617/log⁡log⁡qL(1,\chi)\ge0.0617/\log\log qL(1,χ)≥0.0617/loglogq under ℜs>7/8\Re s>7/8ℜs>7/8 zero-freeness

Explicit Littlewood lower bound $L(1,\chi)\ge0.0617/\log\log q$ under $\Re s>7/8$ zero-freeness