OAI.SiegelZeros.WeightedTorusJets.exists_absolute_real_zero_gap
OpenThe theorem, which is admitted rather than proved in the source, states that there is an absolute constant c > 0 such that the following holds for every integer modulus q ≥ 3 (with q nonzero) and every Dirichlet character χ modulo q with complex values that is primitive, is not the trivial character, and is real-valued, meaning that χ(a) has imaginary part zero for every residue a in ZMod q. For every real number β strictly between 0 and 1 at which the Dirichlet L-function of χ, evaluated at the complex number β, vanishes, the constant satisfies c ≤ (1 − β) · log q. In other words, a real zero of L(s, χ) in the open interval (0,1) cannot lie closer to 1 than c / log q, uniformly over all such q and χ.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/SiegelZeros.lean; bytes 82..445 -- 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 namespace WeightedTorusJets
theorem exists_absolute_real_zero_gap :
∃ 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 WeightedTorusJets
end SiegelZeros
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.