Vinogradov's three primes theorem (unconditional)

Read-back: Davenport.three_primes

The statement asserts the existence of a single natural-number threshold $N_0$ such that every sufficiently large odd natural number is a sum of exactly three primes. Precisely, it claims:

Every symbol here is standard and ranges over the natural numbers. The threshold $N_0$ is a natural number quantified outermost, so it is chosen once and for all, before $n$: a single uniform bound must work simultaneously for every admissible $n$ (the claim is not merely that each odd $n$ has its own threshold). The variable $n$ ranges over all of $\mathbb{N}$, and the conclusion is required only for those $n$ satisfying both hypotheses: $N_0 \le n$ (a non-strict inequality, so $n = N_0$ itself is included) and "$n$ is odd", which for a natural number means there exists $r \in \mathbb{N}$ with $n = 2r + 1$. The three witnesses $p_1, p_2, p_3$ are natural numbers, each required to be prime in the usual sense for natural numbers (an integer $\ge 2$ whose only divisors are $1$ and itself; in particular $0$ and $1$ are excluded, and $2$ is admitted). The final requirement is an exact equality of natural numbers, $p_1 + p_2 + p_3 = n$ — not an inequality, not an approximation, and not a count of representations.

Several things the quantifiers silently permit or leave open should be made explicit:

• The three primes need not be distinct. No condition $p_1 \ne p_2$, $p_1 \ne p_3$, or $p_2 \ne p_3$ appears, so repetitions such as $n = p + p + p$ or $n = p + p + q$ are acceptable witnesses.
• The primes need not be odd. The value $2$ is a legitimate witness, so a decomposition such as $n = 2 + 2 + q$ with $q$ prime satisfies the conclusion; the statement does not demand three odd primes.
• No ordering or size constraints are imposed on $p_1, p_2, p_3$ (no $p_1 \le p_2 \le p_3$, no lower or upper bounds relative to $n$), and the triple is not asserted to be unique — the existential is a plain $\exists$, not $\exists!$, so nothing is claimed about the number of such representations.
• $N_0$ is unconstrained and non-explicit. It is not required to be positive, and no bound, formula, or computability is claimed for it; it may be $0$, in which case the statement would apply to every odd $n$ including $n = 1$, $n = 3$, $n = 5$. Conversely $N_0$ may be arbitrarily large, so the assertion carries no information about any particular small odd number. As a pure existence claim it provides no effective value of $N_0$.
• The hypotheses are jointly satisfiable, so the claim is not vacuous. For any choice of $N_0$ there are infinitely many odd $n \ge N_0$, so the implication genuinely constrains the theorem for infinitely many $n$; the conclusion cannot be discharged by making the antecedent impossible. Even $n$ and odd $n < N_0$ are simply outside the scope of the claim — nothing whatsoever is asserted about them.
• No sum-of-two-primes (even case) content. The statement says nothing about even numbers, nothing about sums of two primes, and nothing about representations by more or fewer than three primes.

The declaration's statement uses only standard notions from the ambient library — natural numbers, the primality predicate, oddness, and addition. None of the auxiliary definitions carried in the accompanying dependency files (a von Mangoldt sum over an arithmetic progression $\psi(N; q, a)$, a zero-free-region boundary $1 - c/\log(q(|\operatorname{Im} s| + 2))$ and the associated membership predicate, an exceptional-set predicate for Dirichlet $L$-functions, a Gauss-type character sum, and a twisted von Mangoldt sum) occur anywhere in the statement, and therefore none of them constrains what is being asserted. The proof body is left unproved.