The three primes singular series vanishes at even $n$

Proved

Vino.singSeriesDvd_eq_zero_of_even

by tabbott · Sep 2, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theorycircle-methodnumber-theorysingular-series

Let $Q$ be squarefree and even, and let $n$ be even. Then

\sum_{q\mid Q}\frac{\mu(q)c_q(n)}{\varphi(q)^3}=0 .

This is the formal statement of the parity obstruction in the three primes problem. As soon as the modulus $Q$ sees the prime $2$ , the local density at $2$ is zero for even $n$ , and the whole singular series collapses — matching the elementary fact that an even number is not a sum of three odd primes.

Preamble

import Definitions.Def_Vino_ramanujan
import Mathlib.Data.Nat.Totient
import Mathlib.Algebra.BigOperators.Ring.Finset
open Finset

Formal statement

namespace Vino

theorem singSeriesDvd_eq_zero_of_even {Q : ℕ} (hQ : Squarefree Q) (h2 : 2 ∣ Q) {n : ℤ} (hn : (2 : ℤ) ∣ n) :
    singSeriesDvd Q n = 0 := by sorry

end Vino

Source

R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997, Chapter 3, Section 3.2 (the singular series of the three primes theorem); I. M. Vinogradov, Representation of an odd number as a sum of three primes, Doklady Akademii Nauk SSSR 15 (1937), 291-294.

View graph

The three primes singular series vanishes at even nnn

The three primes singular series vanishes at even $n$