The Quasi-Riemann Hypothesis (Theorem 1.1)
ProvedQRH.quasi_riemann_hypothesisTheorem 1.1 of the source. Assume the mean-square estimate for the twisted family in the uniform form supplied by the paper: for every Hecke character nu, every weight Wt, every 0 < theta <= 1/10, and every eps > 0, there is k with the mean square of the family over the rows of norm at most D^(1+theta) bounded by k D^(2+theta+eps) for all D >= 2. Then: (1) every finite-order Hecke L-function over K = Q(sqrt(-3)) is nonzero on the half-plane Re s > 11/12, except at s = 1 for the trivial character, where zeta_K has a pole; and (2) every Dirichlet L-function, including the Riemann zeta function, is nonzero there, except at s = 1 for the trivial character. In particular, no Landau-Siegel zero exists.
import Mathlib import Definitions.Def_QRH_arith import Definitions.Def_QRH_sums import Definitions.Def_QRH_lfun
universe u
namespace QRH
/-- The Quasi-Riemann Hypothesis: Theorem 1.1 of the source. The
hypothesis is the mean-square estimate for the twisted family in the
uniform form supplied by the paper — for every Hecke character, every
weight, every 0 < θ ≤ 1/10, and every ε > 0, the mean square of the
family A_u(D) over the rows of norm at most D^(1+θ) is O(D^(2+θ+ε)) —
which the source proves from Poisson summation, the theta
transformation, the quadratic large sieve, and the admissible-exponent
descent. The conclusion has two clauses: every finite-order Hecke
L-function over K = Q(√−3) is nonzero on the half-plane Re s > 11/12 —
obtained by the prime-extraction step with θ small enough for the
requested exponent loss, the Mellin step, and the base change step —
and consequently every Dirichlet L-function, including the Riemann
zeta function, is nonzero there; in particular no Landau-Siegel zero
exists. The value at s = 1 for a trivial character is excluded from
both clauses: ζ and ζ_K have a pole there, not a zero. -/
theorem quasi_riemann_hypothesis (W : QRHWorld.{u}) (S : QRHSums W)
(L : QRHLWorld W S)
(hms : ∀ (ν : L.HeckeChi) (Wt : ℝ → ℂ) (θ ε : ℝ),
0 < θ → θ ≤ 1 / 10 → 0 < ε →
∃ k : ℝ, ∀ D : ℝ, 2 ≤ D →
msSum W S (fun n => W.mu n * L.hcoef ν n) Wt (D ^ (1 + θ)) D (2 * D)
≤ k * D ^ (2 + θ + ε)) :
(∀ (ν : L.HeckeChi) (s : ℂ), 11 / 12 < s.re →
s ≠ 1 ∨ ¬ L.IsTrivialH ν → L.Lk ν s ≠ 0)
∧ (∀ (χ : L.DirChi) (s : ℂ), 11 / 12 < s.re →
¬ L.IsTrivialD χ ∨ s ≠ 1 → L.Ld χ s ≠ 0) := by
sorry
end QRH
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Read-back (self-check authored by the same model that produced the statement): the formal goal theorem takes the world W, the sums data S, the L-function world L, and the uniform mean-square hypothesis hms quantified over every Hecke character, every weight, every 0 < theta <= 1/10, and every eps > 0, and concludes the conjunction of the Hecke clause (for every nu and s with 11/12 < s.re and s != 1 or nu not trivial, Lk nu s != 0) and the Dirichlet clause (for every chi and s with 11/12 < s.re and chi not trivial or s != 1, Ld chi s != 0). The proof shape assembles the reduction chain of the fragment: the prime-extraction step with theta small enough (theta := a fifth of the requested loss) upgrades the mean square to MobiusSaving for mu nu, the Mellin step excludes the Hecke zeros, and the base change step transfers the half-plane to every Dirichlet L-function. The mean-square estimate is the hypothesis the source proves and the mission assumes; the exclusion at (trivial character, s = 1) is the pole point, disclosed on the statement.