The Mellin step: the power saving excludes Hecke zeros on Re s > 11/12
ProvedQRH.mellin_zero_freeFix a finite-order Hecke character nu and a weight Wt, and assume the power-saving predicate MobiusSaving for the coefficient sequence mu nu. Then the Hecke L-function L_K(s, nu) has no zero on the half-plane Re s > 11/12, except possibly at the value s = 1 for the trivial character, where zeta_K has a pole: for every s with Re s > 11/12 and s != 1 or nu nontrivial, L_K(s, nu) != 0. The argument is the Mellin identity of the interface: the Euler product outside S inverts the smoothed transform on the half-plane, the omitted factors are nonzero there, and the weight transform is nonzero, so a zero of L_K would force a nonzero quantity to vanish.
import Mathlib import Definitions.Def_QRH_arith import Definitions.Def_QRH_sums import Definitions.Def_QRH_lfun
universe u
namespace QRH
/-- The Mellin step of section 3 of the source: a power saving for the
smoothed Möbius sums excludes zeros of the Hecke L-function on the
half-plane Re s > 11/12. Under the power saving, the conditional Mellin
identity of the interface — termwise integration, Hecke's meromorphic
continuation, and the identity theorem of the source — reads
L_K^S(s, ν) · M_W(s) = Ŵ(s) on the half-plane, the omitted Euler factors
eS are nonzero there, and the Mellin transform of the weight is nonzero;
a zero of L_K(·, ν) would force the right side to vanish, a
contradiction. The value at s = 1 for the trivial character is excluded
from the claim: ζ_K has a pole there, not a zero. -/
theorem mellin_zero_free (W : QRHWorld.{u}) (S : QRHSums W)
(L : QRHLWorld W S) (ν : L.HeckeChi) (Wt : ℝ → ℂ)
(hms : MobiusSaving W S (fun n => W.mu n * L.hcoef ν n) Wt) :
∀ s : ℂ, 11 / 12 < s.re → s ≠ 1 ∨ ¬ L.IsTrivialH ν → L.Lk ν 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 theorem takes the hypothesis hms : MobiusSaving W S (fun n => mu n * hcoef nu n) Wt and concludes that for every s : C with 11/12 < s.re and (s != 1 or nu not trivial), Lk nu s != 0. The proof shape: the mellin_identity field of the L-function world gives Lk nu s * Mf nu Wt s * eS nu s = Wf nu Wt s on the half-plane; the fields eS_nz and Wf_pos make the second and third factors nonzero there; a zero of Lk nu s would make the left side zero while the right side Wf is nonzero, a contradiction. The disjunction (s != 1 or not trivial) is the disclosed pole exclusion, carried by the statement because the pole of zeta_K at s = 1 is not expressible in the interface.