Read-back: Davenport.zero_free_region

The theorem asserts the existence of one single real constant $c$, chosen once and for all, with $c > 0$, such that the following holds for every modulus $q \in \mathbb{N}$ that is assumed nonzero (the typeclass hypothesis NeZero q, i.e. $q \ge 1$; $q = 1$ is allowed and not excluded) and for every Dirichlet character $\chi$ modulo $q$ with values in $\mathbb{C}$ (that is, every multiplicative character $\chi : \mathbb{Z}/q\mathbb{Z} \to \mathbb{C}$ — no primitivity, no non-triviality, no realness and no other restriction is imposed on $\chi$ at this point; the trivial character $\chi = 1$ is included in the quantification): there exists a set $E \subseteq \mathbb{C}$ of complex numbers, depending on $q$ and $\chi$ (but $c$ does not depend on them), such that $E$ is an "exceptional set" for $c$ and $\chi$ in the sense unfolded below, and such that additionally

where $L(\cdot,\chi)$ denotes Mathlib's analytically continued Dirichlet $L$-function of $\chi$ and $L'$ is its complex derivative taken as a total function (so at any point where $L(\cdot,\chi)$ failed to be complex-differentiable the derivative would be the junk value $0$; every point of $E$ satisfies $0 < \operatorname{Re} z < 1$, hence $z \neq 1$).

Unfolding the region. For a real $c$, a modulus $q$ and a point $s \in \mathbb{C}$, the region boundary is the real number

with $\log$ the real natural logarithm (for $q \ge 1$ the argument $q(|\operatorname{Im} s| + 2) \ge 2$, so the logarithm is at least $\log 2 > 0$ and no division-by-zero junk value arises). The predicate "$s$ is in the region" means

a non-strict inequality, so the boundary curve itself belongs to the region. The region is symmetric in $\operatorname{Im} s \mapsto -\operatorname{Im} s$, it widens as $|\operatorname{Im} s|$ grows, and it contains the entire closed half-plane $\operatorname{Re} s \ge 1$ (since $c > 0$ forces $\beta_c(q,s) < 1$). Nothing in the statement bounds $c$ from above; for a large $c$ the region would extend to the left of $\operatorname{Re} s = 0$, and for a small $c$ it is a thin sliver just to the left of $\operatorname{Re} s = 1$.

Unfolding "$E$ is an exceptional set for $c$ and $\chi$". This is the conjunction of exactly three conditions:

1. $E$ is a subsingleton: $E$ has at most one element (any two elements of $E$ are equal). $E = \varnothing$ is explicitly permitted.

2. Every element of $E$ is a real, non-trivial, quadratic exceptional zero: for every $z \in E$,

   • $\operatorname{Im} z = 0$ (so $z$ is real),
   • $0 < \operatorname{Re} z$ and $\operatorname{Re} z < 1$ (both strict, so $z$ lies in the open interval $(0,1)$ of the real axis),
   • $z$ lies in the region, i.e. $\beta_c(q,z) \le \operatorname{Re} z$,
   • $L(z,\chi) = 0$,
   • $\chi$ is quadratic (every value of $\chi$ is $0$, $1$ or $-1$), and
   • $\chi \neq 1$, i.e. $\chi$ is not the trivial character mod $q$.

   The last two clauses are properties of $\chi$ alone but are stated inside the quantifier over $z \in E$; consequently, whenever $\chi$ is not quadratic, or $\chi = 1$ (in particular whenever $q = 1$, where the only character is the trivial one), this condition forces $E = \varnothing$. When $E = \varnothing$ this whole condition, and likewise the theorem's extra conclusion $L'(z,\chi) \neq 0$, hold vacuously.

3. Non-vanishing off $E$: for every $s \in \mathbb{C}$ with $s \neq 1$, if $s$ lies in the region ($\beta_c(q,s) \le \operatorname{Re} s$) and $s \notin E$, then

The point $s = 1$ is excluded from this claim unconditionally, for every $q$ and every $\chi$ (including the non-trivial ones, so no assertion whatsoever is made about $L(1,\chi)$). Because $E$ has at most one element, at most one point of the region is exempted from the non-vanishing conclusion.

Putting it together. The full assertion is therefore: there is an absolute constant $c > 0$ such that for every $q \ge 1$ and every Dirichlet character $\chi$ mod $q$ one can produce a set $E$ containing at most one complex number, every member of which is a real point of $(0,1)$ lying in the region at which $L(\cdot,\chi)$ vanishes and whose derivative $L'(\cdot,\chi)$ is nonzero there, such a member existing only when $\chi$ is a non-trivial quadratic character; and such that $L(s,\chi) \neq 0$ at every point $s \neq 1$ of the region $\operatorname{Re} s \ge 1 - c/\log(q(|\operatorname{Im} s|+2))$ other than the (at most one) point of $E$.

The existential form means the theorem is satisfied by taking $E = \varnothing$ whenever the non-vanishing condition 3 holds with no exception; in that case conditions 1 and 2 and the derivative conclusion are vacuously true and the entire content of the statement is condition 3. Conversely, when $E$ is a singleton $\{z\}$, the statement asserts both that $z$ is a zero of $L(\cdot,\chi)$ at which the derivative is nonzero (a simple zero, in the sense that $L(z,\chi)=0$ and $L'(z,\chi) \neq 0$) and that it is the only zero of $L(\cdot,\chi)$ in the region apart from the excluded point $s = 1$. No claim is made about zeros outside the region, about the number of characters that can carry such an exceptional zero for a given $q$, or about any quantitative lower bound on $1 - z$.