A multiple real zero of $L(s,\chi)$ lies to the left of $1-c/\log(2q)$ (Davenport §14)

A multiple real zero cannot be too close to $1$. There is an absolute constant $c>0$ with the following property. Let $q\ge1$, let $\chi$ be a non-principal Dirichlet character modulo $q$, and let $\beta\in(0,1)$ be a real number at which $L(s,\chi)$ vanishes to order at least $2$ (a double or higher zero). Then

Here $L(s,\chi)$ is the analytically continued Dirichlet $L$-function and the order of vanishing at $\beta$ is the order of the zero of the analytic function $s\mapsto L(s,\chi)$ at $s=\beta$.

This is the multiplicity half of Davenport's §14 statement that a real non-principal character has at most one simple real zero in the region $\sigma>1-c/\log q$: if $\beta$ were a zero of order $m\ge2$, then for real $\sigma>1$ the inequality $-\dfrac{L'}{L}(\sigma,\chi)\le c_1\log q-\dfrac{m}{\sigma-\beta}$, combined with the trivial lower bound $-\dfrac{L'}{L}(\sigma,\chi)\ge\dfrac{\zeta'}{\zeta}(\sigma)\ge-\dfrac1{\sigma-1}-c_2$, forces $1-\beta\gg1/\log q$ after choosing $\sigma-1\asymp1/\log q$. In the Siegel–Walfisz argument it guarantees that a possibly multiple exceptional zero in a wide region contributes to $\psi(x,\chi)$ only a term of size $x^{\beta}\le x\exp(-c\log x/\log(2q))$, which is absorbed into the error term.

Formalization Note. analyticOrderNatAt (LFunction χ) β is Mathlib's order of vanishing (as a natural number; it is $0$ both when $L(\beta,\chi)\ne0$ and in the degenerate case of an identically vanishing germ, which cannot occur for an $L$-function), so the hypothesis 2 ≤ analyticOrderNatAt … says exactly that $\beta$ is a zero of order at least two. The normalisation $\log(2q)$ (rather than $\log q$) keeps the statement meaningful for $q=1,2$.