Prove2Me

Off-diagonal 74\tfrac74 symmetric von Mangoldt lower bound above 2⋅10182\cdot10^{18}

Open
WeakGoldbach.symmetric_vonMangoldt_off_diagonal_lower_bound_seven_four_above_2e18

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

circle-methodgoldbachnumber-theoryvon-mangoldt

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

F(2m)=∏p∣2mp>2p−1p−2,Om=∑1≤t<m−1Λ(m−t)Λ(m+t).F(2m)=\prod_{\substack{p\mid 2m\\p>2}}\frac{p-1}{p-2},\qquad O_m=\sum_{1\le t<m-1}\Lambda(m-t)\Lambda(m+t).

The bound is

Om≥74F(2m)m.O_m\ge\tfrac74 F(2m)m.

Role: off-diagonal companion of WeakGoldbach.symmetric_vonMangoldt_lower_bound_with_diagonal_seven_four_above_2e18. Splitting the t=0t=0 term gives Wm=Λ(m)2+OmW_m=\Lambda(m)^2+O_m, and the displayed estimate implies the with-diagonal 74\tfrac74 bound. Independent of the 32\tfrac32/triple/7/47/4-total ancestor chain.

This remains an open quantitative sufficient estimate.

Preamble
import Mathlib
Formal statement
namespace WeakGoldbach

theorem symmetric_vonMangoldt_off_diagonal_lower_bound_seven_four_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)).erase 0)
          (fun t => (ArithmeticFunction.vonMangoldt (m - t) : Real) *
            (ArithmeticFunction.vonMangoldt (m + t) : Real)) := by
  sorry

end WeakGoldbach
Source
Reduction lemma for WeakGoldbach.symmetric_vonMangoldt_lower_bound_with_diagonal_seven_four_above_2e18. Parallel to off_diagonal nodes at 5/4 and 3/2. Avoids the 3/2 / triple / total-7/4 ancestor chain.

View graph