The lattice L-functions of the Eisenstein-integer Hecke family have no zeros for Re(s) > 7/8 apart from the excluded pole

Open

SEF.hecke_seven_eighths

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

eisenstein-integershecke-l-functionslatticezero-free-region

For every character of the Hecke family of the Eisenstein integers - the structure Character of the definition bundle SEF_hecke, carrying a nonzero modulus ideal of the Eisenstein integers, a multiplicative character of the residue quotient that is trivial on the units, and a positive period contained in the modulus - and every complex number s with real part greater than 7/8, if it is not the case that the residue character is trivial and s is 1, then the normalized lattice L-function LFunction chi s (the completed L-function of the period-grid theta pair, divided by 6) does not vanish at s. The statement is transcribed verbatim from the source file; the supporting construction is the theta-product layer of the definition bundle SEF_theta and the character layer of SEF_hecke. This is an open problem, the Eisenstein-integer analogue of the mission goal.

Preamble

import Mathlib
import Definitions.Def_SEF_theta
import Definitions.Def_SEF_hecke

Formal statement

/-!
# SEF: the $7/8$ zero-free line for the Hecke-family lattice $L$-functions

For every `Character` of the Eisenstein integers (see `Def_SEF_hecke`), the
normalized lattice $L$-function `LFunction χ s` does not vanish in the
half-plane $\operatorname{Re}(s) > 7/8$, apart from the excluded pole
(residue character trivial, $s = 1$). Source: user-supplied Lean 4 statement
file `HeckeSevenEighths.lean.txt` (namespace
`OAI.SevenEighths.HeckeFamily`), statement transcribed verbatim; it is
published in the mission namespace as `SEF.hecke_seven_eighths`, with the two
identifiers of the definition bundles (`Character`, `LFunction`) written fully
qualified. The supporting construction is the theta-product layer of `Def_SEF_theta` and
the character layer of `Def_SEF_hecke`. This is an open problem, the
Eisenstein-integer analogue of the mission goal. Draft: the proof is a
`sorry`.
-/

namespace SEF

theorem hecke_seven_eighths
    (χ : OAI.SevenEighths.HeckeFamily.Character) {s : ℂ} (hs : (7 / 8 : ℝ) < s.re)
    (hpole : ¬ (χ.residue = 1 ∧ s = 1)) :
    OAI.SevenEighths.HeckeFamily.LFunction χ s ≠ 0 := by
  sorry

end SEF

Source

HeckeSevenEighths.lean.txt, user-supplied Lean 4 statement file (namespace OAI.SevenEighths.HeckeFamily), theorem LFunction_ne_zero_of_seven_eighths_lt_re, transcribed verbatim.

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: for every character chi of the Hecke family over the Eisenstein integers and every complex number s, if the real part of s is greater than 7/8 and it is not the case that both the residue multiplicative character of chi is the trivial character (the constant 1) and s equals 1, then the lattice L-function of chi evaluated at s is not zero. Hypotheses: the real part of s exceeds 7/8; the negated conjunction excludes exactly the pole configuration (the trivial residue character at the point 1); the character carries its own conditions in its fields - a modulus ideal that is not the zero ideal, triviality of the residue character on the units, and a positive period contained in the modulus.

View graph