Circle-method integral lower bound with constant $7/2$ above $2\cdot10^{18}$

Open

WeakGoldbach.integral_main_term_seven_halves_above_2e18

by Ethan Cheung Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

circle-methodgoldbachnumber-theoryvon-mangoldt

For an integer $m>2\cdot10^{18}$ , put

F(2m)=\prod_{\substack{p\mid2m\\p>2}}\frac{p-1}{p-2},\qquad S(\alpha,N)=\sum_{n<N}\Lambda(n)e(\alpha n).

The proposed estimate is

\operatorname{Re}\int_0^1 S(\alpha,2m)^2 e(-2m\alpha)\,d\alpha\ge\tfrac72\,F(2m)\,m.

Role: this is the circle-method integral form of WeakGoldbach.symmetric_vonMangoldt_total_with_7_4_margin_above_2e18. By the identity $R(2m)=2W_m-\Lambda(m)^2$ , a lower bound of $\tfrac72 F(2m)m$ on the real part of the integral yields $W_m\ge\tfrac74 F(2m)m$ once the diagonal is dropped (nonnegative). The constant $\tfrac72$ is exactly twice the full-sum coefficient $\tfrac74$ .

This is an open quantitative sufficient condition, parallel to WeakGoldbach.integral_main_term_above_2e18 (constant $\tfrac52$ ) and WeakGoldbach.integral_main_term_triple_above_2e18 (constant $3$ ), but independent of those nodes so as not to create a dependency cycle with the $\tfrac32$ /triple chain.

Formalization Note Exponential sums and $e(\cdot)$ are from Definitions.Def_Vino_primes and Definitions.Def_CircleMethod_char.

Preamble

import Mathlib
import Definitions.Def_Vino_primes
import Definitions.Def_CircleMethod_char

Formal statement

namespace WeakGoldbach

theorem integral_main_term_seven_halves_above_2e18 (m : ℕ) (hm : 2 * 10 ^ 18 < m) :
    ((∫ α in (0:ℝ)..1, (Vino.vmSum α (2*m))^2
        * CircleMethod.e (-((2*m : ℕ) : ℝ) * α)).re : ℝ)
      ≥ (7 / 2 : ℝ)
        * (∏ p ∈ (2 * m).primeFactors.filter (2 < ·),
            ((p : ℝ) - 1) / ((p : ℝ) - 2)) * m := by
  sorry

end WeakGoldbach

Source

Circle-method integral form of WeakGoldbach.symmetric_vonMangoldt_total_with_7_4_margin_above_2e18; normalization as in J. Pintz, arXiv:1804.09084, Section 2, equation (2.9). Parallel to WeakGoldbach.integral_main_term_above_2e18 / integral_main_term_triple_above_2e18 with constant 7/2. This reference does not assert or prove the displayed explicit-threshold estimate.

View graph

Circle-method integral lower bound with constant 7/27/27/2 above 2⋅10182\cdot10^{18}2⋅1018

Circle-method integral lower bound with constant $7/2$ above $2\cdot10^{18}$