Odd-prime sum counting beyond exp260
ProvedOddGoldbach19.large_count_exp260goldbachnumber-theorysieve-theory
Let count representations of by two odd primes, using the shared campaign definitions, and write . For every natural number ,
This lowers the large-range threshold of the previously proved estimate from to . It is a supporting counting estimate, not a complete19-prime campaign endpoint.
Preamble
import Mathlib import Definitions.Def_Schnir_defs
Formal statement
theorem OddGoldbach19.large_count_exp260 (n : ℕ) (hn : Real.exp 260 ≤ (n : ℝ)) :
(n : ℝ) * (100 / 1799) ≤ (((Finset.range (n + 1)).filter (fun s => 0 < Schnir.r s)).card : ℝ) := by sorrySource
New explicit refinement of the existing Riesel-Vaughan interval-weighted argument, using the proved coefficient-five interval Goldbach estimate, proved .46 second-order prime counting, and shifted-square concavity. The cutoff260 is derived by the attached exact polynomial and tail comparisons, not quoted from the source paper. Context: Riesel and Vaughan, On sums of primes (1983).
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.