Prove2Me

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

Open
WeakGoldbach.symmetric_vonMangoldt_lower_bound_with_diagonal_seven_four_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).

The bound is

Wm≥74F(2m)m+12Λ(m)2.W_m\ge \tfrac74 F(2m)m+\tfrac12\Lambda(m)^2.

Role: diagonal-corrected companion of WeakGoldbach.integral_main_term_seven_halves_above_2e18. Doubling and subtracting the diagonal in R(2m)=2Wm−Λ(m)2R(2m)=2W_m-\Lambda(m)^2 yields Re⁡R(2m)≥72F(2m)m\operatorname{Re} R(2m)\ge\tfrac72 F(2m)m. Analogue of the 54\tfrac54 and 32\tfrac32 with-diagonal nodes; independent of those ancestors.

This remains an open quantitative sufficient estimate.

Preamble
import Mathlib
Formal statement
namespace WeakGoldbach

theorem symmetric_vonMangoldt_lower_bound_with_diagonal_seven_four_above_2e18
    (m : ℕ) (hm : 2 * 10 ^ 18 < m) :
    (7 / 4 : ℝ) *
        (∏ 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_seven_halves_above_2e18. Parallel to with_diagonal nodes at 5/4 and 3/2. Identity R(2m)=2W_m−Λ(m)^2 from binary_count_symmetric.

View graph