An exact integer convolution coefficient

Proved

OddGoldbach19.packed_numeric8000

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

number-theoryverified-computation

Let $Q_*,R_*,W_*$ be the three fixed integers in the shared packed data. Their base- $2^{64}$ coefficient at position $2\cdot40907$ is

\left\lfloor\frac{Q_*R_*W_*}{(2^{64})^{2\cdot40907}}\right\rfloor\bmod2^{64}=557349373474.

This is an exact finite arithmetic statement. Relating the packed integers to the prime-shift family and the singular-weight lookup table is a separate proof obligation.

Preamble

import Definitions.Def_OddGoldbach19_PackedData8000

Formal statement

theorem OddGoldbach19.packed_numeric8000 :
    ((OddGoldbach19.Packed8000.packedQ*OddGoldbach19.Packed8000.packedR*
      OddGoldbach19.Packed8000.packedW)/(2^64)^(2*40907))%(2^64)=557349373474 := by sorry

Source

Exact numerical component of a private finite-shift certificate for the known Riesel-Vaughan prime-sum method. The coefficient computation uses chunked natural-number encodings; it does not itself assert their finite-sum interpretation.

View graph