Read-back: Davenport.deriv_LFunction_bound

Literal rendering. The declaration asserts the existence of a single real number $K$ such that $K > 0$ and such that the following holds for every modulus, every character, and every point simultaneously: for every natural number $q$ that is nonzero (a typeclass side-condition $\mathrm{NeZero}\,q$, i.e. $q \neq 0$, carried as an instance argument), for every Dirichlet character $\chi$ of modulus $q$ with values in the complex numbers $\mathbb{C}$, if $\chi$ is not equal to the trivial (principal) character modulo $q$ and if $3 \le q$, then for every real number $\sigma$ satisfying the two inequalities

one has

Here $L(\cdot,\chi)$ is Mathlib's analytically continued Dirichlet $L$-function attached to $\chi$, $L'$ denotes its complex derivative (the derivative of the function $s \mapsto L(s,\chi)$ of a complex variable, a total operation which returns the junk value $0$ at any point where the function fails to be complex-differentiable), $\|\cdot\|$ is the modulus of a complex number, $\log q$ is the natural logarithm of the natural number $q$ cast into $\mathbb{R}$, and $(\log q)^2$ is the square of that logarithm — not $\log(q^2)$.

Quantifier order and uniformity of $K$. The existential $\exists K$ is the outermost binder, so $K$ is one absolute constant: it does not depend on $q$, on $\chi$, or on $\sigma$. All of $q$, $\chi$, $\sigma$ are universally quantified inside the scope of $K$. The positivity requirement $0 < K$ is strict; the concluding bound is non-strict ($\le$).

The point at which the derivative is evaluated. The evaluation point is $(\sigma : \mathbb{C})$, i.e. the real number $\sigma$ coerced into $\mathbb{C}$ with zero imaginary part. The statement therefore constrains the derivative only on the real axis — at the points $s = \sigma + 0i$ — and says nothing about any $s$ with nonzero imaginary part. It is a bound on a real segment, not on a vertical strip or a region of the complex plane, and there is no auxiliary height parameter $t$ anywhere in the statement.

The range of $\sigma$. The admissible $\sigma$ form the closed real interval $\left[\,1 - \tfrac{1}{\log q},\; 1\,\right]$, with both endpoints included. In particular $\sigma = 1$ is an admissible point (the bound is asserted at $s = 1$ itself), and so is the left endpoint $1 - 1/\log q$. Note the interval is bounded above by $1$, so nothing is claimed for $\sigma > 1$, where the Dirichlet series converges.

Degenerate and boundary behaviour of the interval.

• Because $q \ge 3$ is assumed, $\log q \ge \log 3 \approx 1.0986 > 1$, hence $0 < 1/\log q < 1$ and the left endpoint $1 - 1/\log q$ lies strictly between $0$ and $1$. The interval is always nonempty (it contains $\sigma = 1$) and is always a subinterval of $(0,1]$.
• At the smallest admissible modulus $q = 3$: $1/\log 3 \approx 0.9102$, so the interval is approximately $[0.0898,\, 1]$ — a long segment reaching almost down to the origin, extending far to the left of the line $\sigma = 1/2$ and covering all but a sliver of the critical strip along the real axis. Similarly for $q = 4$ ($1/\log 4 \approx 0.7213$, interval $\approx [0.279, 1]$), $q = 5$ ($\approx [0.379, 1]$), and other small $q$: the constraint is substantive over a wide range of $\sigma$.
• As $q \to \infty$, $1/\log q \to 0$, so the left endpoint tends to $1$ from below and the interval shrinks down to the single point $\{1\}$. For large $q$ the assertion concerns only an increasingly thin neighbourhood of $s = 1$ on the real axis, while the right-hand side $K(\log q)^2$ grows without bound.
• The division $1/\log q$ is a total operation; were $\log q$ zero the expression would evaluate to $1 - 0 = 1$ and the interval would collapse to $\{1\}$. The hypothesis $3 \le q$ excludes this ($q = 1$ would give $\log 1 = 0$), so the degenerate division does not actually arise under the stated hypotheses.

Hypotheses on $q$ and $\chi$. Two conditions on $q$ appear: the instance assumption $q \neq 0$ and the explicit inequality $3 \le q$; the latter subsumes the former, so the instance is redundant as a mathematical constraint (it is present because forming $\mathbb{Z}/q\mathbb{Z}$ and hence a Dirichlet character modulo $q$ requires it). No primality, squarefreeness, or other arithmetic restriction is placed on $q$: it ranges over all integers $q \ge 3$. Likewise $\chi$ ranges over all Dirichlet characters modulo $q$ other than the principal one — primitive and imprimitive alike, real and complex, even and odd. The hypothesis $\chi \neq 1$ removes exactly one character (the principal character mod $q$), and for every $q \ge 3$ there is at least one character satisfying it, so the hypotheses are simultaneously satisfiable and the statement is not vacuous.

What is bounded. The quantity bounded is the modulus of the derivative of the $L$-function itself, $|L'(\sigma,\chi)|$ — not the logarithmic derivative $L'/L$, not $|L(\sigma,\chi)|$, and not any quotient or reciprocal. The bound is $K(\log q)^2$, a quantity depending on $q$ only (through $\log q$) and not on $\sigma$ or on $\chi$: for a fixed modulus the same numerical bound is claimed uniformly across all nonprincipal characters mod $q$ and all $\sigma$ in the stated interval.

Scope of the statement. The statement is a closed proposition with no free variables and no hypotheses outside itself; it contains no reference to any definition introduced elsewhere in the bundle — every notion it uses ($L$-functions, complex derivative, norm, real logarithm, Dirichlet characters, the trivial character) is taken from the ambient library. The proof is not supplied in the code shown.