An absolute logarithmic Siegel bound: (1 - beta) log q is bounded away from zero for real zeros

Open

SEF.siegel_zero_bound

by Lucas · Oct 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

dirichlet-l-functionssiegel-zeroszero-free-region

There is an absolute positive real constant c such that, for every modulus q of at least 3, every primitive non-principal real-valued Dirichlet character chi mod q, and every real beta with 0 < beta < 1 at which the L-function of chi vanishes, the inequality c <= (1 - beta) log q holds. The statement is transcribed verbatim from the source file, in the unbundled hypothesis form in which the source states it. This is an open problem of logarithmic strength: it goes far beyond Siegel's ineffective theorem, which gives only (1 - beta) >= c(epsilon) q^(-epsilon), and beyond the best effective bounds. It is a consequence of the mission goal, the seven-eighths zero-free line for Dirichlet L-functions.

Preamble

import Mathlib
import Definitions.Def_SEF_theta
import Definitions.Def_SEF_hecke

Formal statement

/-!
# SEF: a Siegel-type bound of logarithmic strength for real zeros

There is an absolute constant $c > 0$ such that every real zero
$\beta \in (0, 1)$ of the $L$-function of a primitive, non-principal,
real-valued Dirichlet character of modulus $q \ge 3$ satisfies
$(1 - \beta) \log q \ge c$. Source: user-supplied Lean 4 statement file
`SiegelZeros.lean.txt` (namespace `OAI.SiegelZeros.WeightedTorusJets`),
statement transcribed verbatim; it is published in the mission namespace as
`SEF.siegel_zero_bound`. This is an open problem, of logarithmic
strength: it is far beyond Siegel's ineffective theorem, which gives only
$1 - \beta \gg_\varepsilon q^{-\varepsilon}$, and beyond the best effective
bounds. It is a consequence of the mission goal. Draft: the proof is a
`sorry`.
-/

namespace SEF

theorem siegel_zero_bound :
    ∃ c : ℝ, 0 < c ∧
      ∀ (q : ℕ) [NeZero q], 3 ≤ q →
      ∀ χ : DirichletCharacter ℂ q,
        χ.IsPrimitive → χ ≠ 1 → (∀ a : ZMod q, (χ a).im = 0) →
        ∀ β : ℝ, 0 < β → β < 1 → χ.LFunction (β : ℂ) = 0 →
          c ≤ (1 - β) * Real.log (q : ℝ) := by
  sorry

end SEF

Source

SiegelZeros.lean.txt, user-supplied Lean 4 statement file (namespace OAI.SiegelZeros.WeightedTorusJets), theorem exists_absolute_real_zero_gap, transcribed verbatim.

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: there exists a real constant c, together with a proof that c is positive, such that for every modulus q (a nonzero natural number) of at least 3, every Dirichlet character chi modulo q that is primitive, not the principal character, and real-valued (every value has zero imaginary part), and every real beta with 0 < beta < 1 at which the L-function of chi evaluated at beta vanishes, the constant c is at most the product (1 - beta) log q. Hypotheses: q is at least 3; chi is primitive, non-principal, and real-valued; beta is strictly between 0 and 1 and is a zero of the L-function. The constant is absolute: it does not depend on q, chi, or beta.

View graph