A strengthened prime-sum count for logarithms between26 and100

Proved

OddGoldbach19.medium_count_log100

by Yuxuan Xu · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-number-theorynumber-theorysieve-theory

For $n\in\mathbb N$ , let $R(n)$ count the integers $s\le n$ that are sums of two odd primes. If $26\le\log n\le100$ , then

R(n)\ge\frac{100}{1799}n.

The estimate provides part of the uniform count needed for a Schnirelmann-density argument. It uses the known1000-prime finite-shift certificate together with explicit prime-pair estimates and a tighter upper bound for the twin-prime constant.

Preamble

import Mathlib
import Definitions.Def_Schnir_defs

Formal statement

theorem OddGoldbach19.medium_count_log100 (n : ℕ)
    (hln : 26≤Real.log (n:ℝ)) (hlu : Real.log (n:ℝ)≤100) :
    (n:ℝ)*(100/1799:ℝ)≤(((Finset.range (n+1)).filter (fun s=>0<Schnir.r s)).card:ℝ) := by sorry

Source

Finite-shift second moment method of Riesel and Vaughan, On sums of primes (1983). The finite combinatorial identities are generalized from public Apache2.0 accepted Prove2Me proof2e6ffca0-db78-43ae-93a9-bc1793b1bf07 and related campaign proofs; the explicit interval and endpoint arithmetic here use the accepted private supporting estimates.

View graph