Read-back: Davenport.siegel_walfisz_char

What the declaration is. Davenport.siegel_walfisz_char is a closed theorem — it takes no arguments, no variables, and no typeclass assumptions. Its statement is exactly the proposition ThreePrimes.SiegelWalfisz, which is a single Prop with no parameters. Unfolding that proposition, and unfolding Vino.vmSumChar inside it, the theorem asserts the following.

The character sum. For a natural number $q$, a Dirichlet character $\chi$ modulo $q$ with values in $\mathbb{C}$ (i.e. a multiplicative character on the ring $\mathbb{Z}/q\mathbb{Z}$ into $\mathbb{C}$), and a natural number $N$, write

where $\Lambda$ is the von Mangoldt function (regarded as a real number and then coerced into $\mathbb{C}$), and $n \bmod q$ is the image of $n$ in $\mathbb{Z}/q\mathbb{Z}$. Two features of this sum are literal and worth stating: the index set is $\{0,1,\dots,N-1\}$, so the summation runs over $n$ strictly below $N$ and includes $n=0$ (with $\Lambda(0)=0$ and $\Lambda(1)=0$, so those terms vanish); and $\chi$ is a multiplicative character on $\mathbb{Z}/q\mathbb{Z}$, so $\chi$ takes the value $0$ at every non-unit residue, meaning the sum is effectively over those $n < N$ with $\gcd(n,q)=1$.

The assertion. The theorem states:

For every real number $A$ with $0 < A$, there exist real numbers $C$ and $c$ such that $0 < c$ and, for every natural number $q$ with $1 \le q$, for every Dirichlet character $\chi$ modulo $q$ with values in $\mathbb{C}$, and for every natural number $N$ with $2 \le N$, if

(real power of the natural logarithm; $\le$, not $<$), then

where $\|\cdot\|$ is the complex absolute value, $\chi = 1$ means $\chi$ is the trivial (principal) character modulo $q$, and $N$ in the main term is the natural number $N$ coerced to $\mathbb{C}$.

Quantifier order and what depends on what. The constants $C$ and $c$ are chosen after $A$ and before $q$, $\chi$, and $N$: they may depend only on $A$, and are uniform in the modulus $q$, in the character $\chi$, and in the length $N$. Only $c$ is required to be positive; $C$ carries no positivity or sign hypothesis at all (it is merely asserted to exist as a real number), and there is no other relation imposed between $C$ and $c$. Nothing asserts that $C$ or $c$ is effectively computable, nor is any explicit value given.

Hypotheses on $q$, $\chi$, $N$. The only hypothesis on the modulus is $1 \le q$ (so $q = 0$ is excluded, but $q = 1$ is allowed). Nothing requires $\chi$ to be primitive, non-principal, quadratic, of bounded conductor, or induced by anything; the single Dirichlet character quantifier ranges over all characters mod $q$, principal and non-principal alike, including the character that is identically $0$ on non-units. The only hypothesis on the length is $2 \le N$, together with the size constraint $q \le (\log N)^{A}$. No hypothesis relates $N$ to $q$ beyond that inequality, and there is no lower bound on $N$ of the form "$N$ sufficiently large in terms of $A$" other than what the inequality itself forces.

Degenerate and edge cases silently included.

• Small $N$ is vacuous. Since $q \ge 1$ and $A > 0$, the hypothesis $q \le (\log N)^{A}$ forces $(\log N)^{A} \ge 1$, hence $\log N \ge 1$, hence $N \ge 3$. In particular the case $N = 2$ (where $\log 2 \approx 0.693$ and $(\log 2)^A < 1$) satisfies the hypotheses for no $q \ge 1$ at all, so the conclusion there is vacuously true; the effective range is $N \ge 3$.
• The modulus $q = 1$. $\mathbb{Z}/1\mathbb{Z}$ is the trivial ring, so the only Dirichlet character mod $1$ is the trivial one; the branch $\chi = 1$ is taken, $\chi(n) = 1$ for every $n$, and the claim becomes a Prime Number Theorem statement with error term $\exp(-c\sqrt{\log N})$: $\bigl|\sum_{n<N}\Lambda(n) - N\bigr| \le C N \exp(-c\sqrt{\log N})$.
• The principal character's main term. Whenever $\chi$ is the trivial character mod $q$ (for any $q \ge 1$), the quantity subtracted is exactly $N$ — not $N-1$, not $\frac{\varphi(q)}{q}N$, not $\psi(N)$, and not an integral. For every non-principal $\chi$ the subtracted quantity is exactly $0$, so the claim is a bound on $\|S(q,\chi,N)\|$ itself.
• Off-by-one. Because the sum stops at $n = N-1$ while the main term is $N$, the comparison is between $\sum_{n \le N-1}\Lambda(n)\chi(n)$ and $N$.
• The if is decided classically (open Classical in supplies decidability of the equality $\chi = 1$); it has no mathematical content beyond selecting the two branches above.
• Bound shape. The right-hand side is $C \cdot N \cdot e^{-c\sqrt{\log N}}$ with $\sqrt{\cdot}$ the real square root and $\log$ the real natural logarithm; the exponent is $-c\sqrt{\log N}$, i.e. square-root-of-log savings, not $-c(\log N)^{3/5}$ and not a power saving.

Unused material in the bundle. The dependency file Definitions/Def_Davenport_siegelWalfisz.lean also defines $\psi(N;q,a) = \sum_{n<N} \Lambda(n)\,[\,n \equiv a \bmod q\,]$ (psiAP), a zero-free-region boundary $1 - c/\log\bigl(q(|\Im s|+2)\bigr)$ (regionBoundary), the predicate $\text{`InRegion`}$ saying that boundary is $\le \Re s$, and IsExceptionalSet (a subsingleton set of real zeros in $(0,1)$ of $L(\cdot,\chi)$ for quadratic non-principal $\chi$, outside which $L(s,\chi) \neq 0$ on the region for $s \neq 1$), and Vino.gaussE defines a Gauss sum. None of these definitions occur in the statement of Davenport.siegel_walfisz_char; the statement uses only Vino.vmSumChar as unfolded above.

Proof status (factual). The declaration's proof body is sorry.