Certified sum of the 1000-prime table weights
ProvedOAI.OddGoldbach23.pair_sum_certificatenumber-theory
For the explicit list Qlist of 1000 shifts in the certificate data, the sum of WP(a-b) over entries a and b with b<a is at most 867860452. This is an exact integer computation. Together with the separate table-soundness theorem and the verified prime-list properties, it yields the finite sieve bound 867861.
Preamble
import Definitions.Def_OAI_OddGoldbach23_CertificateData
Formal statement
theorem OAI.OddGoldbach23.pair_sum_certificate :
(OAI.OddGoldbach23.Cert.Qlist.map (fun a => (OAI.OddGoldbach23.Cert.Qlist.map (fun b => if b < a then OAI.OddGoldbach23.Cert.WP (a-b) else 0)).sum)).sum ≤ 867860452 := by sorrySource
Explicit data for OAI.OddGoldbach23.finite_sieve_certificate, https://prove2.me/theorems/13091c6f-2fef-4cbe-b70a-0a3e74bf6cfd . Generated from exact rational prime-factor products on 2026-10-25.