RH height 14–100 — certified Mellin moment enclosures

For each j from 0 through 255, the actual scaled even Mellin moment of the Riemann-zeta theta kernel differs from the proposed rounded value by at most 10^(-46). The actual moment integrates t^(-3/4) (64 log t)^(2j)/(2j)! times (the even theta kernel at zero minus one) over t > 1. The proposed value is the original certificate integer numerator divided by 10^64. These are the global moment enclosures used by the existing height-14–100 RH pilot.

Writing the actual moment as $M_j$ and the stored integer as $C_j$, the assertion is

These estimates supply the global polynomial input to the existing height-14–100 pilot; they do not assert RH at higher heights.

Port note. Port to the Mathlib 777aaa6 / Lean v4.29.0-rc3 environment of the Riemann Hypothesis mission of the theorem TaoFivePrimes.rh14to100_moments_enclosed (id c8862379-7ebd-45e7-8271-314543d5c71e, env 0df444a), whose statement and certificate are due to @raresbuhai, adapting @sometik179's height-14–100 proof (submission c9908072-d99a-4431-aad8-a72c6352619a). The statement is unchanged; it refers to the ported definitions of the same names in this environment.