Littlewood lower bound for $L(1,\chi)$ under a zero-free half-plane $\Re s>7/8$

Statement. There exist a real constant $c>0$ and a natural number $q_0$ such that the following holds. For every natural number $q\ge q_0$ with $q\neq 0$, and every Dirichlet character $\chi$ modulo $q$ with values in $\mathbb{C}$ satisfying

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$,

one has

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).

Quantifier structure and edge cases.

• $c$ and $q_0$ come first and are uniform: they may not depend on $q$ or $\chi$. Nothing bounds $c$ from below beyond $c>0$ and nothing bounds $q_0$; the prover chooses both.
• Hypothesis 3 is a zero-free half-plane hypothesis ($\operatorname{Re}s>7/8$) placed on each individual $\chi$; the theorem is conditional on it, character by character. It includes $s=1$ and the whole region $\operatorname{Re}s\ge 1$.
• For $q\ge 3$, primitivity rules out the trivial character, so a primitive real character is a primitive quadratic character; for moduli $q$ that carry no such character the hypotheses are unsatisfiable and the claim for that $q$ is vacuous. Modulo $2$ there is no primitive character at all. Modulo $1$ the trivial character is primitive and $L(s,\chi)=\zeta(s)$, with Mathlib's junk value $\zeta(1)=(\gamma-\log 4\pi)/2<0$; this case is only included if the chosen $q_0\le 1$.
• $\log$ is the real logarithm with Mathlib's conventions $\log 0=0$, $\log x=\log|x|$ for $x<0$, and $c/0=0$. For small $q$ (e.g. $q\le 15$, where $\log\log q\le 0$ or $\log q$ is small) the left side may be $0$, negative, or very large; such $q$ are excluded only if $q_0$ is chosen large enough.
• The conclusion is about the real part of $L(1,\chi)$; it does not separately assert that $L(1,\chi)$ is real.