Quadratic sifted prime mass for the Section 8 trapezoid

Proved

TaoFivePrimes.eta1_quadratic_prime_mass

by Yuxuan Xu · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

circle-methodfourier-analysisnumber-theory

Let x be a positive integer and let eta1 be the trapezoidal cutoff from Section 8 of Tao's five-primes paper. Set

M_x=\sum_{n=0}^{x}\Lambda(n)\mathbf1_{(n,\sqrt{x}\#)=1}\eta_1(n/x)^2.

Here the square-root primorial includes primes at most the integer square root of x, exactly as in the platform definition. Assume

10^8\le x/10,\qquad 10^4(3/2)\le x,\qquad 5(3/2)\le\log(x/10),\qquad 10^8(9/4)\le x.

Then there is a real epsilon such that

|\varepsilon|\le0.02,\qquad M_x=\frac23(1+\varepsilon)x.

This is the quadratic prime-mass input (4.13) of Corollary 4.9 specialized to the Section 8 cutoff. The factor 2/3 is its squared L2 norm; it must not be replaced by 1. The explicit prime estimate, removal of prime powers, and passage from the smooth statement to the literal piecewise-linear cutoff remain part of this theorem's proof obligation. This statement does not assert a major-arc energy lower bound.

Preamble

import Definitions.Def_TaoFivePrimes_ArcSplit
open scoped BigOperators
open TaoFivePrimes

Formal statement

theorem TaoFivePrimes.eta1_quadratic_prime_mass (x : ℕ)
    (hc8 : (10 ^ 8 : ℝ) ≤ (1 / 10 : ℝ) * x)
    (hneat : (10 ^ 4 : ℝ) * (3 / 2 : ℝ) ≤ x)
    (halamo : 5 * (3 / 2 : ℝ) ≤ Real.log ((1 / 10 : ℝ) * x))
    (h10q : (10 ^ 8 : ℝ) * (9 / 4 : ℝ) ≤ x) :
    ∃ ε : ℝ, |ε| ≤ 0.02 ∧
      (∑ n ∈ Finset.range (x + 1), siftedVonMangoldt x n * eta1 ((n : ℝ) / x) ^ 2) =
        (2 / 3 : ℝ) * (1 + ε) * x := by sorry

Source

Terence Tao, Every odd number greater than 1 is the sum of at most five primes, https://arxiv.org/abs/1201.6656v4. Corollary 4.9, equation (4.13), printed p. 20, specialized to the Section 8 cutoff and its squared norm 2/3; includes the nonsmooth-cutoff justification.

View graph