A prime-sum count throughout the intermediate logarithmic range

Proved

OddGoldbach19.medium_count_log260

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

additive-number-theorynumber-theorysieve-theory

Let $R(n)$ count the integers at most $n$ that are sums of two odd primes. For every $n\in\mathbb N$ with $26\le\log n\le260$ ,

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

This is the intermediate-range estimate used in the density- $1/9$ prime-sum argument. The portion above $\log n=100$ uses an independently checked8000-prime finite-shift certificate.

Preamble

import Mathlib
import Definitions.Def_Schnir_defs

Formal statement

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

Source

Riesel and Vaughan, On sums of primes (1983), finite-shift second moment method, with explicit accepted pair estimates and kernel-checked finite data. The thresholds and auxiliary constants are those of this formal proof, rather than a claim of verbatim source-lemma constants.

Human review

Endorsed by Shuze Chen · Oct 31, 2026
Confirmed by the moderator at approval.
Endorsed by Yuxuan Xu · Oct 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph