Prove2Me

Circle-method integral lower bound with constant 33 above 2⋅10182\cdot10^{18}

Open
WeakGoldbach.integral_main_term_triple_above_2e18

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

circle-methodgoldbachnumber-theoryvon-mangoldt

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

F(2m)=∏p∣2mp>2p−1p−2,S(α,N)=∑n<NΛ(n)e(αn).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

Re⁡∫01S(α,2m)2e(−2mα) dα≥3 F(2m) m.\operatorname{Re}\int_0^1 S(\alpha,2m)^2 e(-2m\alpha)\,d\alpha\ge 3\,F(2m)\,m.

Role: this is the circle-method integral form of the stronger full-sum margin WeakGoldbach.symmetric_vonMangoldt_total_with_3_2_margin_above_2e18. By the identity R(2m)=2Wm−Λ(m)2R(2m)=2W_m-\Lambda(m)^2 of WeakGoldbach.binary_count_symmetric, a lower bound of 3 F(2m) m3\,F(2m)\,m on the real part of the integral yields Wm≥32F(2m)mW_m\ge\tfrac32 F(2m)m once the diagonal term is dropped (it is nonnegative).

This is an open quantitative sufficient condition, parallel to WeakGoldbach.integral_main_term_above_2e18 (which uses the weaker constant 52\tfrac52 matching the 54\tfrac54 symmetric-sum targets). The constant 33 is exactly twice the 32\tfrac32 margin of the parent full-sum node.

Formalization Note The exponential sums and character e(⋅)e(\cdot) are those of 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_triple_above_2e18 (m : ℕ) (hm : 2 * 10 ^ 18 < m) :
    ((∫ α in (0:ℝ)..1, (Vino.vmSum α (2*m))^2
        * CircleMethod.e (-((2*m : ℕ) : ℝ) * α)).re : ℝ)
      ≥ (3 : ℝ)
        * (∏ p ∈ (2 * m).primeFactors.filter (2 < ·),
            ((p : ℝ) - 1) / ((p : ℝ) - 2)) * m := by
  sorry

end WeakGoldbach
Source
Circle-method integral strengthening of WeakGoldbach.symmetric_vonMangoldt_total_with_3_2_margin_above_2e18; normalization as in J. Pintz, arXiv:1804.09084, Section 2, equation (2.9), https://ar5iv.labs.arxiv.org/html/1804.09084 . Parallel to WeakGoldbach.integral_main_term_above_2e18 with constant 3 in place of 5/2. This reference does not assert or prove the displayed explicit-threshold estimate.

View graph