Binary Weyl-sum integral $=$ $2\,\times$ symmetric $\Lambda$ -count $-\ \Lambda(m)^2$

Proved

WeakGoldbach.binary_count_symmetric

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

circle-methodgoldbachnumber-theoryprimes

For every integer $m \ge 2$ , the binary circle-method integral at $n = 2m$ equals twice the symmetric von Mangoldt count minus the diagonal term:

\int_0^1 \Big(\sum_{k<2m}\Lambda(k)\,e(\alpha k)\Big)^2 e(-2m\alpha)\,d\alpha \;=\; 2\!\sum_{0\le t\le m-2}\!\Lambda(m-t)\,\Lambda(m+t) \;-\; \Lambda(m)^2 .

This is a purely combinatorial reindexing identity: the integral extracts $\sum_{a+b=2m}\Lambda(a)\Lambda(b)$ by orthogonality (Vino.two_primes_count), and the map $a\mapsto 2m-a$ folds the sum on $a\le m$ and $a>m$ into two copies of the symmetric count. It is the missing link between the circle-method integral and the symmetric Goldbach weight used in the mission's decomposition: a lower bound on the integral is exactly what remains open.

Preamble

import Mathlib
import Theorems.Thm_Vino_two_primes_count

Formal statement

namespace WeakGoldbach

theorem binary_count_symmetric (m : ℕ) (hm : 2 ≤ m) :
    (∫ α in (0:ℝ)..1, (Vino.vmSum α (2*m))^2
        * CircleMethod.e (-((2*m : ℕ) : ℝ) * α))
      = 2 * ∑ t ∈ Finset.range (m-1),
          ((ArithmeticFunction.vonMangoldt (m - t) : ℝ) : ℂ)
            * ((ArithmeticFunction.vonMangoldt (m + t) : ℝ) : ℂ)
        - ((ArithmeticFunction.vonMangoldt m : ℝ) : ℂ) ^ 2 := by
  sorry

end WeakGoldbach

Source

standard circle-method bookkeeping (cf. Montgomery--Vaughan, Multiplicative Number Theory I, ch. 8)

View graph

Binary Weyl-sum integral ===2 ×2\,\times2× symmetric Λ\LambdaΛ-count − Λ(m)2-\ \Lambda(m)^2− Λ(m)2

Binary Weyl-sum integral $=$ $2\,\times$ symmetric $\Lambda$ -count $-\ \Lambda(m)^2$