A uniform zero-free region off the critical line for the real-analytic Eisenstein series up to height 0.78·2πy

Let E(z,s) be the real-analytic Eisenstein series for SL(2,ℤ), with z = x + iy, and let Λ(z,s) = π^(−s) Γ(s) E(z,s). We prove that for every y ≥ 2 and every real x, all zeros of Λ(z,·) with 0 < Im s < T(y) lie on the critical line Re s = 1/2, and that the zeros on the line below T(y) are simple. Here T(y) ≥ 0.783·2πy for 2 ≤ y < 7.2, T(y) ≥ 0.878·2πy for 7.2 ≤ y ≤ 112 (≥ 0.944·2πy once y ≥ 30), and T(y) ≥ 0.898·2πy for y ≥ 112. Stark’s classical theorem (1967) reaches |Im s| ≤ 2y = 0.318·2πy, and only for y above a non-explicit constant. The proof deforms Λ into its constant term through Λ_λ = 2a₀ + λH, λ ∈ [0,1], and uses the theorem of Lagarias and Suzuki on the zeros of a₀. Every way an off-line zero could enter the region is then excluded. On the critical line this reduces to an explicit inequality M < 1, controlled by turning-point bounds for Kᵢₜ(2πny). For y ≥ 112 all estimates are analytic. They use explicit bounds for ζ′/ζ and 1/ζ near Re s = 1, together with the inequality |ζ*(2−2s)/ζ*(2s)| ≤ |s/(s−1)| for Re s ≥ 1/2, which follows from the Hadamard product. For 2 ≤ y ≤ 112 the estimates are certified with ball arithmetic (Arb/FLINT) on 1230 intervals of y. Numerical censuses suggest that the first off-line zeros appear near 0.99·2πy. The work was carried out with the assistance of an AI system (Claude, Anthropic). The paper describes the tools, the workflow and an independent review. Code and the full certification log are included.