Positivity of Tao’s weighted representation count (K = 1000)

Open

TaoFivePrimes.representationCount_pos

by Patrick · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

circle-methodexponential-sumsgoldbachnumber-theory

Let $x$ be any integer in the range

8.7\cdot10^{36}\leq x\leq e^{3100}.

For the weighted count $R$ of equation (8.10), using Tao's cutoffs, inclusive square-root primorial sieves, and the fixed parameter $K=1000$ , prove

R(x,4\cdot10^{14})>0.

This is the analytic input isolated by the proof of Theorem 8.2. Combined with the prime-witness extraction theorem, it gives three odd primes whose sum lies in $[x-4\cdot10^{14},x-2]$ . The claim applies to even as well as odd $x$ ; it remains an open proof obligation in this formalization.

The exact Fourier identity is now proved, including integrability. It identifies the count with the circle-method integral. The explicit analytic estimates needed to make this integral positive remain separate, unresolved work.

Preamble

import Definitions.Def_TaoFivePrimes_RepresentationCount
open TaoFivePrimes

Formal statement

theorem TaoFivePrimes.representationCount_pos (x : ℕ)
    (h1 : 87 * 10 ^ 35 ≤ x) (h2 : (x : ℝ) ≤ Real.exp 3100) :
    0 < TaoFivePrimes.representationCount x (4 * 10 ^ 14) := by sorry

Source

Terence Tao, https://arxiv.org/abs/1201.6656, proof of Theorem 8.2 in Section 8: positivity target (8.10), Fourier expression (8.11), fixed K=10^3, and the subsequent major-arc and minor-arc estimates.

View graph