Prove2Me

Diagonal-corrected 32\tfrac32 symmetric von Mangoldt lower bound above 2⋅10182\cdot10^{18}

Open
WeakGoldbach.symmetric_vonMangoldt_lower_bound_with_diagonal_triple_above_2e18

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

goldbachnumber-theoryvon-mangoldt

For every natural number m>2⋅1018m>2\cdot10^{18}, let

F(2m)=∏p∣2mp>2p−1p−2,Wm=∑t=0m−2Λ(m−t)Λ(m+t),F(2m)=\prod_{\substack{p\mid 2m\\p>2}}\frac{p-1}{p-2},\qquad W_m=\sum_{t=0}^{m-2}\Lambda(m-t)\Lambda(m+t),

where Λ\Lambda is the von Mangoldt function. The bound is

Wm≥32F(2m)m+12Λ(m)2.W_m\ge \frac32 F(2m)m+\frac12\Lambda(m)^2.

Role: this is the diagonal-corrected symmetric-sum estimate needed to deduce WeakGoldbach.integral_main_term_triple_above_2e18 from the identity R(2m)=2Wm−Λ(m)2R(2m)=2W_m-\Lambda(m)^2. Doubling the displayed inequality and subtracting the diagonal term yields Re⁡R(2m)≥3 F(2m) m\operatorname{Re} R(2m)\ge 3\,F(2m)\,m. It is the exact analogue of WeakGoldbach.symmetric_vonMangoldt_lower_bound_with_diagonal_above_2e18, with coefficient 32\tfrac32 in place of 54\tfrac54 (matching the integral constants 33 and 52\tfrac52 respectively).

This remains an open quantitative sufficient estimate at the finite threshold m>2⋅1018m>2\cdot10^{18}.

Preamble
import Mathlib
Formal statement
namespace WeakGoldbach

theorem symmetric_vonMangoldt_lower_bound_with_diagonal_triple_above_2e18
    (m : ℕ) (hm : 2 * 10 ^ 18 < m) :
    (3 / 2 : ℝ) *
        (∏ p ∈ (2 * m).primeFactors.filter (2 < ·), ((p : ℝ) - 1) / ((p : ℝ) - 2)) *
        (m : ℝ)
      + ((ArithmeticFunction.vonMangoldt m : ℝ) ^ 2) / 2
      ≤ ∑ t ∈ Finset.range (m - 1),
          (ArithmeticFunction.vonMangoldt (m - t) : ℝ) *
            (ArithmeticFunction.vonMangoldt (m + t) : ℝ) := by
  sorry

end WeakGoldbach
Source
Reduction lemma for WeakGoldbach.integral_main_term_triple_above_2e18. Parallel to WeakGoldbach.symmetric_vonMangoldt_lower_bound_with_diagonal_above_2e18 (coefficient 3/2 in place of 5/4). The identity R(2m)=2W_m−Λ(m)^2 is recorded in WeakGoldbach.binary_count_symmetric; normalization as in Pintz arXiv:1804.09084 §2 (2.9).

View graph