Exact packed encodings of the finite prime shifts and their reversal

Proved

OddGoldbach19.packed_prime_factors8000

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

number-theoryverified-computation

Let $B=2^{64}$ , $D=40907$ , and let $\mathcal Q$ be the fixed8000-prime list. The shared packed integers satisfy

Q_*=\sum_{q\in\mathcal Q}B^{(q-3)/2},\qquad R_*=\sum_{q\in\mathcal Q}B^{D-(q-3)/2}.

These identities connect the stored integers to the exact finite prime-position data.

Preamble

import Mathlib
import Definitions.Def_OddGoldbach19_CertificateData8000
import Definitions.Def_OddGoldbach19_PackedData8000
open scoped BigOperators

Formal statement

theorem OddGoldbach19.packed_prime_factors8000 :
    (OddGoldbach19.Cert8000.Qlist.map (fun q=>(2^64)^((q-3)/2))).sum=
      OddGoldbach19.Packed8000.packedQ ∧
    (OddGoldbach19.Cert8000.Qlist.map (fun q=>(2^64)^(40907-(q-3)/2))).sum=
      OddGoldbach19.Packed8000.packedR := by sorry

Source

Exact finite packed-integer certificate for the known Riesel-Vaughan finite-shift method; all original-data identifications are independently kernel checked.

View graph