Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-05
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Positive logarithmic Dirichlet series force boundary nonvanishing

Statement

Let F be holomorphic on Re⁡s>1 and suppose that for σ>1,

log⁡F(σ+it)=∑n≥2bnn−σ−it

with bn≥0, the series converging absolutely. Assume moreover that F is meromorphic on a neighbourhood of the closed half-plane Re⁡s≥1, has at most a simple pole at s=1, and has no other pole there. Then F has no zero on Re⁡s=1.

Facts & Assumptions

Given: A function F with the stated properties.

[L1]

A Dirichlet series with nonnegative coefficients and finite abscissa of convergence is singular at its abscissa of convergence (Landau's theorem for Dirichlet series with nonnegative coefficients).

Proof

technique · contradiction
1.1givenassume-contraalgebra

Suppose first that F(1+it0)=0 for some real t0≠0. For σ>1, absolute convergence gives log⁡∣F(σ+iu)∣=∑n≥2bnn−σcos⁡(ulog⁡n), so log⁡ ⁣(∣F(σ)∣3∣F(σ+it0)∣4∣F(σ+2it0)∣)=∑n≥2bnn−σ(3+4cos⁡θn+cos⁡(2θn)) with θn=t0log⁡n. Since 3+4cos⁡θ+cos⁡(2θ)=2(1+cos⁡θ)2≥0, the product on the left is at least 1.

2.1step 1.1L1givendischarge-contradiction∎

Because F is meromorphic with at most a simple pole at 1, the factor F(σ) grows like O((σ−1)−1) as σ↓1, while F(σ+2it0) stays bounded and the zero at 1+it0 forces F(σ+it0)=O(σ−1). Therefore the product from step 1.1 is O(σ−1)→0, contradicting the lower bound 1. The Landau statement [L1] concerns singularity of the logarithmic series at its own abscissa, so it does not by itself exclude a zero of F at 1. Instead, if F(1)=0, then F is holomorphic at 1 and F(σ)→0 as σ↓1, whereas the assumed logarithmic identity at t=0 gives log⁡∣F(σ)∣=∑n≥2bnn−σ≥0 and hence ∣F(σ)∣≥1 for every σ>1. This is another contradiction. Thus no zero occurs on the line Re⁡s=1.

Depends on

Used by

Dependency tree · two levels

4 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources