Prove2Me

A 7/47/4 margin for the full symmetric von Mangoldt sum above 2⋅10182\cdot10^{18}

Open
WeakGoldbach.symmetric_vonMangoldt_total_with_7_4_margin_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}, the full symmetric von Mangoldt sum satisfies

Wm=∑0≤t<m−1Λ(m−t)Λ(m+t)  ≥  74 F(2m) m,F(2m)=∏p∣2mp>2p−1p−2.W_m=\sum_{0\le t<m-1}\Lambda(m-t)\Lambda(m+t) \;\ge\; \tfrac74\,F(2m)\,m, \qquad F(2m)=\prod_{\substack{p\mid 2m\\p>2}}\frac{p-1}{p-2}.

Role: this is the full-sum companion of WeakGoldbach.symmetric_vonMangoldt_off_diagonal_lower_bound_triple_above_2e18. Combined with the proved diagonal bound Λ(m)2≤14F(2m)m\Lambda(m)^2\le\tfrac14 F(2m)m, it yields the off-diagonal estimate

Wm−Λ(m)2≥(74−14)F(2m)m=32F(2m)m.W_m-\Lambda(m)^2\ge\bigl(\tfrac74-\tfrac14\bigr)F(2m)m=\tfrac32 F(2m)m.

The coefficient 74\tfrac74 is exactly 32+14\tfrac32+\tfrac14, so the diagonal absorption introduces no extra slack beyond the known 14\tfrac14 diagonal majorant. The construction is parallel to the reduction of the 54\tfrac54 off-diagonal node from the 32\tfrac32 full-sum margin, but uses a fresh full-sum leaf so as not to depend on that 32\tfrac32 margin or its integral/diagonal descendants.

This remains an open quantitative sufficient estimate at the stated finite threshold.

Preamble
import Mathlib
Formal statement
namespace WeakGoldbach

theorem symmetric_vonMangoldt_total_with_7_4_margin_above_2e18 (m : Nat) (hm : 2 * 10 ^ 18 < m) :
    (7 / 4 : Real) * Finset.prod ((2 * m).primeFactors.filter (fun p => 2 < p))
        (fun p => ((p : Real) - 1) / ((p : Real) - 2)) * (m : Real) <=
      Finset.sum (Finset.range (m - 1))
        (fun t => (ArithmeticFunction.vonMangoldt (m - t) : Real) *
          (ArithmeticFunction.vonMangoldt (m + t) : Real)) := by
  sorry

end WeakGoldbach
Source
Full-sum companion for WeakGoldbach.symmetric_vonMangoldt_off_diagonal_lower_bound_triple_above_2e18. Diagonal absorption uses WeakGoldbach.vonMangoldt_diagonal_small_above_2e18 (proved, coefficient 1/4). Parallel to the pair (total 3/2 margin, off-diagonal 5/4); here the pair is (total 7/4, off-diagonal 3/2). Hardy–Littlewood singular-series heuristics motivate the shape; no source asserts this finite-threshold inequality.

View graph