The absolute logarithmic Siegel bound, bundled hypothesis form

Open

SEF.siegel_zero_bound_bundled

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 for which three conditions hold bundled together - beta is positive, beta is strictly less than 1, and the L-function of chi vanishes at beta - the inequality c <= (1 - beta) log q holds. The statement is transcribed verbatim from the source file, which states the bundled reformulation alongside the unbundled one; the two source statements carry the same mathematical content, differing only in the bundling of the hypotheses on beta, and both are included because the source states both.

Preamble

import Mathlib
import Definitions.Def_SEF_theta
import Definitions.Def_SEF_hecke

Formal statement

/-!
# SEF: the logarithmic Siegel bound, bundled hypothesis form

The bundled reformulation of the logarithmic Siegel bound, included because
the source file states it: an absolute constant $c > 0$ bounds
$(1 - \beta) \log q$ from below for every real zero of a primitive real
Dirichlet $L$-function of modulus $q \ge 3$, with the hypotheses on $\beta$
bundled into a conjunction. Source: user-supplied Lean 4 statement file
`SiegelZeros.lean.txt` (namespace `OAI.SiegelZeros`, declaration
`WeightedTorusJets.dirichletRealZeroBound_proof`, named as in the source),
statement transcribed verbatim; it is published in the mission namespace as
`SEF.siegel_zero_bound_bundled`. Draft: the proof is a `sorry`.
-/

namespace SEF

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

end SEF

Source

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

Read-back

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

Restate: there exists a positive real constant c 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, and every real beta satisfying the conjunction that beta is positive, beta is strictly less than 1, and the Dirichlet L-function of chi evaluated at beta is zero, the constant c is at most (1 - beta) log q. Hypotheses: q is at least 3; chi is primitive, non-principal, and real-valued; the three conditions on beta arrive bundled as a single conjunction, exactly as in the source declaration, whose name is kept verbatim.

View graph