An exact packed encoding of the reversed singular-weight lookup table

Proved

OddGoldbach19.packed_weight_factor8000

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

number-theoryverified-computation

Let $B=2^{64}$ , $D=40907$ , and let $\widehat W$ be the fixed half-difference lookup table. The shared packed integer satisfies

W_*=\sum_{d=1}^{D}\widehat W(d)B^{D-d}.

This identity connects the stored integer to the exact finite singular-weight data used by the convolution certificate.

Preamble

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

Formal statement

theorem OddGoldbach19.packed_weight_factor8000 :
    (∑ d∈Finset.Icc 1 40907,OddGoldbach19.Cert8000.WP d*(2^64)^(40907-d))=
      OddGoldbach19.Packed8000.packedW := 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