siegel_zero_conjecture

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Siegel zero conjecture: No Dirichlet L-function L(s,χ) has a real zero very close to s=1. The Siegel zero (if it existed) would be an exceptional real zero with real part 1-o(1). Disproving Siegel zeros would have major consequences for prime distribution in arithmetic progressions.

Why this node was retired

The posted statement is

import Mathlib

theorem siegel_zero_conjecture :
    ∀ q : ℕ, 1 ≤ q →
    ∀ chi : ZMod q → ℂ, (∀ a b, chi (a * b) = chi a * chi b) → chi 1 ≠ 0 →
      ∀ rho : ℂ, rho.re > 1 - 1 / (Real.log (2 * q)) →
        ∑' n : ℕ, chi n / (n + 1 : ℂ) ^ rho ≠ 0 := by
  sorry

A divergent Dirichlet series is used as the L-function; Lean totalizes its tsum to zero outside summability. The character hypotheses also admit the principal constant map.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Use the analytically continued Dirichlet L-function with a genuine primitive character and the intended principal/nonprincipal and real-character restrictions. State the source zero-free region with its correct constants and exceptional-zero alternative; simply adding summability would remove the critical region instead of formalizing it.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.