Siegel's theorem: $L(1,\chi) > C(\varepsilon)\,q^{-\varepsilon}$ (Davenport §21)

Read-back of Davenport.siegel.

Fix a real number $\varepsilon$ and assume $\varepsilon > 0$ (no upper bound on $\varepsilon$ is imposed). The statement asserts: there exists a real number $C$ such that $C > 0$ and such that, for every natural number $q$ that is nonzero (the instance hypothesis $\mathrm{NeZero}\ q$, i.e. $q \ge 1$) and for every Dirichlet character $\chi$ modulo $q$ with values in $\mathbb{C}$ satisfying the three hypotheses

• $\chi$ is quadratic: every value of $\chi$ lies in $\{0, 1, -1\}$,
• $\chi \neq 1$, i.e. $\chi$ is not the trivial (principal) character modulo $q$,
• $\chi$ is primitive: the conductor of $\chi$ equals $q$,

one has the strict inequality

where $q^{-\varepsilon}$ is the real power of the real number $q$ with exponent $-\varepsilon$, and $L(1,\chi)$ denotes the value at $s = 1$ of the analytically continued Dirichlet $L$-function attached to $\chi$ (Mathlib's DirichletCharacter.LFunction), of which only the real part is taken.

Quantifier order matters here: $C$ is chosen after $\varepsilon$ but before $q$ and $\chi$, so a single positive constant $C$, allowed to depend only on $\varepsilon$, must work simultaneously for all admissible moduli $q$ and all admissible characters $\chi$ mod $q$. Conversely, $C$ is only required to exist — nothing pins down its value, no explicit formula is demanded, and no claim of effectivity or computability is made.

Several features of the claim are worth spelling out literally. The conclusion is a lower bound and it is strict ($<$, not $\le$). It bounds the real part $\operatorname{Re}\, L(1,\chi)$ only; the statement does not assert that $L(1,\chi)$ is a real number, and it makes no claim about $|L(1,\chi)|$ or about $L(1,\chi)$ being nonzero as a complex number (though a positive lower bound on the real part does force $L(1,\chi) \ne 0$). There is no "for all sufficiently large $q$" clause and no exclusion of small moduli: the inequality is asserted for every $q \ge 1$ admitting such a $\chi$. The modulus $q = 0$ is excluded by the $\mathrm{NeZero}$ instance, so the degenerate real power $0^{-\varepsilon}$ never arises; for $q \ge 1$ we have $q^{-\varepsilon} > 0$, so the left-hand side $C\, q^{-\varepsilon}$ is genuinely positive.

The hypotheses are vacuously unsatisfiable for some moduli, in which case the assertion says nothing about them: for $q = 1$ and $q = 2$ the group of units of $\mathbb{Z}/q\mathbb{Z}$ is trivial, so the only Dirichlet character mod $q$ is the trivial one and the hypothesis $\chi \ne 1$ can never hold; more generally, for any $q$ admitting no primitive nontrivial quadratic character the universally quantified statement is empty. The theorem therefore constrains $C$ only through those $q$ that do carry a primitive nontrivial quadratic character.

Finally, note what the statement does not involve. The imported definitions from the bundle — $\psi(N; q, a)$ (psiAP, a truncated von Mangoldt sum over an arithmetic progression), regionBoundary, InRegion, IsExceptionalSet (a zero-free-region-with-at-most-one-exception predicate), and the character sums gaussE and vmSumChar — appear nowhere in the assertion; they are only ambient definitions in the dependency files. The statement mentions no exceptional zero, no Siegel zero, no zero-free region, and no arithmetic progression: it is exactly the single inequality $C q^{-\varepsilon} < \operatorname{Re}\, L(1,\chi)$ under the three hypotheses above, for a constant $C > 0$ depending only on $\varepsilon$.