The base change step: Dirichlet zero-freeness from Hecke zero-freeness

Proved

QRH.dirichlet_base_change

by Lucas · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

basechangedirichletl-functionsriemannzetafunctionzero-freeregion

Assume every Hecke L-function of the world is zero-free on the half-plane Re s > 11/12, with the value at s = 1 for the trivial character excluded. Then every Dirichlet L-function of the L-function world is nonzero at every s with Re s > 11/12 and (chi nontrivial or s != 1). The quadratic base change identity L_K(s, chi o N) = L(s, chi) L(s, chi chi_{-3}) up to Euler factors nonzero on Re s > 0 turns a zero of L(s, chi) away from s = 1 into a zero of a Hecke L-function, contradicting the hypothesis; at s = 1, the Dirichlet nonvanishing theorem L(1, chi_{-3}) != 0 of the interface excludes the only possible pole-zero cancellation.

Preamble

import Mathlib
import Definitions.Def_QRH_arith
import Definitions.Def_QRH_sums
import Definitions.Def_QRH_lfun

Formal statement

universe u

namespace QRH

/-- The base change step of section 3 of the source: the zero-free
half-plane for the Hecke L-functions of K = Q(√−3) implies the zero-free
half-plane for every Dirichlet L-function. The quadratic base change
identity L_K(s, χ ∘ N) = L(s, χ) L(s, χ χ₋₃) up to Euler factors nonzero
on Re s > 0 turns a zero of L(s, χ) into a zero of a Hecke L-function
away from s = 1; at s = 1, the Hecke zero-free hypothesis applies to the
base change of every nontrivial χ, and for χ = χ₋₃ the Dirichlet
nonvanishing theorem L(1, χ₋₃) ≠ 0 of the interface excludes the only
possible pole-zero cancellation, which is the argument the source gives
for the second sentence of Theorem 1.1. -/
theorem dirichlet_base_change (W : QRHWorld.{u}) (S : QRHSums W)
    (L : QRHLWorld W S)
    (hHecke : ∀ (ν : L.HeckeChi) (s : ℂ), 11 / 12 < s.re →
      s ≠ 1 ∨ ¬ L.IsTrivialH ν → L.Lk ν s ≠ 0)
    (χ : L.DirChi) (s : ℂ)
    (hs : 11 / 12 < s.re) (hχ : ¬ L.IsTrivialD χ ∨ s ≠ 1) :
    L.Ld χ s ≠ 0 := by
  sorry

end QRH

Source

The Quasi-Riemann Hypothesis, October 2026, Section 3 (the transfer at the end of the proof of Theorem 1.1).

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 Hecke zero-free hypothesis hHecke (for all nu and s with 11/12 < s.re and s != 1 or nu not trivial, Lk nu s != 0), a Dirichlet character chi, a point s with 11/12 < s.re and chi not trivial or s != 1, and concludes Ld chi s != 0. The proof shape: away from s = 1 the base change identity bc_eq factors Lk (bc chi) s as Ld chi s * Ld (mulChi chi chiM3) s * eulerF chi s with the Euler factor nonzero by eulerF_nz, so a zero of Ld chi s would give a Hecke zero; the triviality transfer bc_triv_iff controls the triviality of the base change; at s = 1 the identity bc_at_one and the nonvanishing Ld_M3_one for the factor mulChi chi chiM3 exclude the cancellation. The trivial Dirichlet character is the Riemann zeta function of the fragment.

View graph