Finite sieve pair-sum certificate, rows 1–250
ProvedOAI.OddGoldbach23.pair_quarter_0number-theory
For rows 1 through 250 of the explicit 1000-entry list Q, the sum of the stored integer weight P(a-b) over all entries b of Q with b<a is at most 53619369. These are consecutive disjoint rows of the finite pair-sum certificate. Adding the four row-block bounds gives 867860452.
Preamble
import Definitions.Def_OAI_OddGoldbach23_CertificateData
Formal statement
theorem OAI.OddGoldbach23.pair_quarter_0 : (((OAI.OddGoldbach23.Cert.Qlist.drop 0).take 250).map (fun a => (OAI.OddGoldbach23.Cert.Qlist.map (fun b => if b < a then OAI.OddGoldbach23.Cert.WP (a-b) else 0)).sum)).sum ≤ 53619369 := by sorry
Source
Finite computational decomposition of https://prove2.me/theorems/91862081-bcf4-4bf9-8499-5e9a39e27aaf . Exact integer computation for the 1000-prime Riesel–Vaughan sieve parameter, 2026-10-25.