Prove2Me

An exact finite bound for the8000-shift rounded pair sum

Proved
OddGoldbach19.finite_pair_sum8000

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

number-theorysieve-theoryverified-computation

Let Q\mathcal Q be the shared list of8000 odd primes through81817, and let W^\widehat W be the shared rounded half-difference lookup table. Then

∑a∈Q∑b∈Qb<aW^ ⁣(a−b2)≤557349373474.\sum_{a\in\mathcal Q}\sum_{\substack{b\in\mathcal Q\\b<a}}\widehat W\!\left(\frac{a-b}{2}\right)\le557349373474.

After division by10000 this gives55,734,937.3474, below the55,737,000 bound used in the finite-shift second moment estimate.

Preamble
import Definitions.Def_OddGoldbach19_CertificateData8000
Formal statement
theorem OddGoldbach19.finite_pair_sum8000 :
    (OddGoldbach19.Cert8000.Qlist.map fun a=>(OddGoldbach19.Cert8000.Qlist.map fun b=>
      if b<a then OddGoldbach19.Cert8000.WP ((a-b)/2) else 0).sum).sum≤557349373474 := by sorry
Source
Exact finite-shift certificate for the Riesel-Vaughan prime-sum method, On sums of primes (1983). The computation is verified through packed natural-polynomial convolution, with separately checked original-data factor identities and an exact integer coefficient.
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