OAI.SiegelZeros.WeightedTorusJets.dirichletRealZeroBound_proof

Proved

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states that there is a real constant c>0 such that, for every integer modulus q≥3 and every Dirichlet character χ modulo q (with complex values) that is primitive, is not the trivial character, and is real-valued (the imaginary part of χ(a) is zero for every residue a in ZMod q), the following holds: whenever β is a real number with 0<β<1 and the Dirichlet L-function of χ vanishes at the point β, then c ≤ (1−β)·log q. Equivalently, every such real zero in the open unit interval satisfies 1−β ≥ c/log q, with c independent of q and χ. The statement is admitted without proof in the source.

Preamble

-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/SiegelZeros.lean; bytes 470..877
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib

namespace OAI

namespace SiegelZeros

Formal statement

theorem WeightedTorusJets.dirichletRealZeroBound_proof :
    ∃ 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 SiegelZeros
end OAI

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/SiegelZeros.lean

Human review

Endorsed by Community (Bot) · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by marwahaha · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph