Explicit two-sided bound for $\log L(1,\chi)$ under $\Re s>7/8$ zero-freeness

Statement. Let $q$ be a natural number with $q\neq 0$ and $10^{100}\le q$. Let $\chi$ be a $\mathbb{C}$-valued Dirichlet character modulo $q$ such that

1. $\chi$ is primitive (its conductor equals $q$);
2. $\chi$ is real-valued: $\operatorname{Im}\chi(a)=0$ for all $a\in\mathbb{Z}/q\mathbb{Z}$;
3. $L(s,\chi)\neq 0$ for every complex $s$ with $\operatorname{Re}s>7/8$.

Then

where $3.2914=32914/10000$ exactly, $\log$ is the natural logarithm, and $\operatorname{Log}$ is the principal branch of the complex logarithm, $\operatorname{Log}z=\log|z|+i\arg z$ with $\arg z\in(-\pi,\pi]$ (and Mathlib's convention $\operatorname{Log}0=0$). The absolute value is the complex modulus, so the left side equals $\sqrt{(\log|L(1,\chi)|)^2+(\arg L(1,\chi))^2}$.

Here $L(s,\chi)$ is Mathlib's Dirichlet $L$-function: the unique meromorphic continuation to all of $\mathbb{C}$ of $\sum_{n\ge1}\chi(n)n^{-s}$ (built from Hurwitz zeta functions); it is a total function $\mathbb{C}\to\mathbb{C}$, and at a pole (only possible at $s=1$ for the trivial character) it returns a fixed finite junk value. "Primitive" means the conductor of $\chi$ (the least $d\mid q$ through which $\chi$ factors) equals $q$. "Real-valued" means $\operatorname{Im}\chi(a)=0$ for every residue class $a\in\mathbb{Z}/q\mathbb{Z}$, including non-units (where $\chi(a)=0$ anyway).

Edge cases.

• For $q\ge10^{100}$, $\log\log\log q\ge\log 5.44\approx1.69>0$, so the right side is a positive, genuine value.
• As in the companion statements, $q\ge3$ plus primitivity excludes the trivial character, so $\chi$ is primitive quadratic and $L(1,\chi)$ is a genuine value; the statement is vacuous for moduli with no primitive real character. Hypothesis 3 is a conditional zero-free half-plane assumption for this $\chi$.
• The bound is two-sided in $\log|L(1,\chi)|$: it gives both $|L(1,\chi)|\le e^{R}$ and $|L(1,\chi)|\ge e^{-R}$ with $R=\log\log\log q+3.2914$. It also bounds the argument: if $L(1,\chi)$ were a negative real number, the left side would include the term $\pi^2$ under the square root. The statement does not itself assert that $L(1,\chi)$ is positive or real.