Read-back: Davenport.siegel_zero

Statement. Let $\varepsilon$ be a real number, and assume $0 < \varepsilon$. The theorem asserts that there exists a real number $C$ such that both of the following hold: $0 < C$, and for every natural number $q$ that is nonzero (the typeclass hypothesis NeZero q, i.e. $q \ge 1$) and every Dirichlet character $\chi$ modulo $q$ with values in $\mathbb{C}$ — that is, a multiplicative character on $\mathbb{Z}/q\mathbb{Z}$ taking complex values, extended by $0$ on the non-units — if

1. $\chi$ is quadratic (every value of $\chi$ is $0$, $1$ or $-1$), and
2. $\chi$ is not the trivial (principal) character modulo $q$, and
3. $\chi$ is primitive (its conductor equals $q$),

then for every real number $\sigma$ satisfying the strict inequality

(here $q^{-\varepsilon}$ is the real power $(q:\mathbb{R})^{-\varepsilon}$, which for $q \ge 1$ lies in $(0,1]$), one has

where $L(\cdot,\chi)$ denotes Mathlib's analytically continued Dirichlet $L$-function of $\chi$ and $\sigma$ is regarded as the complex number $\sigma + 0i$. The inequality $\neq 0$ is an inequality of complex numbers.

Quantifier order. The three quantifier layers are, in order: $\varepsilon$ (with $0 < \varepsilon$) is fixed first; then $C > 0$ is produced, depending only on $\varepsilon$; then $q$, $\chi$ and $\sigma$ are all universally quantified after $C$. So the single constant $C$ must work simultaneously for every modulus $q \ge 1$, every quadratic non-trivial primitive character mod $q$, and every real $\sigma$ in the stated range. The constant is asserted only to exist; no formula, bound, or computability for it is claimed, and no relationship between $C$ and $\varepsilon$ is stated beyond $C > 0$. The three character hypotheses are stated as a chain of implications (quadratic, then non-trivial, then primitive) and are all required together.

What the region of $\sigma$ includes. The constraint on $\sigma$ is a lower bound only; there is no upper bound. In particular the conclusion is asserted for:

• $\sigma = 1$ (nonvanishing of $L(1,\chi)$ is part of the claim, since $1 > 1 - Cq^{-\varepsilon}$ whenever $C > 0$ and $q \ge 1$);
• every $\sigma > 1$, including arbitrarily large $\sigma$;
• if the witness $C$ happens to satisfy $C \ge 1$, then for those $q$ with $q^{\varepsilon} \le C$ the threshold $1 - Cq^{-\varepsilon}$ is $\le 0$, so the range of $\sigma$ sweeps down through $0$ and into negative reals for those moduli; if instead $C < 1$, the threshold is always $> 1 - C > 0$ for all $q \ge 1$, and no non-positive $\sigma$ is covered.

What is not claimed. $\sigma$ ranges only over real numbers; the statement says nothing about zeros of $L(s,\chi)$ at complex $s$ with nonzero imaginary part, and nothing about characters that are non-quadratic, imprimitive, or trivial, nor about $q = 0$. It does not assert that at most one exceptional character/zero exists, nor any quantitative lower bound on $|L(\sigma,\chi)|$ — only non-vanishing.

Degenerate cases. The hypotheses on $\chi$ are unsatisfiable for some moduli, making the inner claim vacuous there: for $q = 1$ and $q = 2$ the unit group of $\mathbb{Z}/q\mathbb{Z}$ is trivial, so the only Dirichlet character mod $q$ is the trivial one and the hypothesis $\chi \neq 1$ fails; more generally, for any $q$ admitting no primitive quadratic character (e.g. $q \equiv 2 \pmod 4$) the hypotheses are never met. The hypotheses are satisfiable for other moduli (e.g. the quadratic character mod $3$), so the statement is not vacuous overall. Note also that $\varepsilon$ is an arbitrary positive real with no upper restriction: for large $\varepsilon$ the factor $q^{-\varepsilon}$ is small and the asserted region is a thin strip to the right of $1 - Cq^{-\varepsilon}$, while for small $\varepsilon$ the region is wider; the theorem asserts the existence of a suitable $C$ separately for each such $\varepsilon$.

Definitions from the bundle. None of the auxiliary definitions carried by the imported dependency files — $\psi$ over an arithmetic progression, the region boundary $1 - c/\log(q(|\operatorname{Im} s| + 2))$, membership in that region, the notion of an exceptional set, the Gauss sum, or the von Mangoldt character sum — appear anywhere in this statement. The only non-Mathlib-primitive notions used are IsQuadratic, IsPrimitive, and the analytically continued LFunction, all from Mathlib.

Proof status. The declaration's proof is sorry; no proof is supplied.