The local factor at $2$ vanishes for even $n$

Proved

Vino.threePrimeFactor_two_of_even

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

analytic-number-theorycircle-methodnumber-theorysingular-series

The local factor of the singular series of the three primes problem at a prime $p$ is

\mathfrak S_p(n)=\begin{cases}1-\dfrac{1}{(p-1)^2},& p\mid n,\\[8pt] 1+\dfrac{1}{(p-1)^3},& p\nmid n.\end{cases}

At $p=2$ and $n$ even this is $1-1/(2-1)^2=0$ :

\mathfrak S_2(n)=0\qquad\text{whenever }2\mid n.

This single vanishing is the parity obstruction of the three primes problem: an even number has no representation as a sum of three odd primes, and the singular series records that fact locally at $2$ .

Preamble

import Definitions.Def_Vino_ramanujan
import Mathlib.Data.Nat.Totient
open Finset

Formal statement

namespace Vino

theorem threePrimeFactor_two_of_even {n : ℤ} (h : (2 : ℤ) ∣ n) : threePrimeFactor 2 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 local factor at 222 vanishes for even nnn

The local factor at $2$ vanishes for even $n$