RH height 14–100 — certified moment data panels0
DefinitionTaoFivePrimes_RH14To100CheckedMomentNCPanels0numerical-verificationriemann-zetatao-five-primes
Four proposed moment-certificate data records, for panel indices 0 through 3. Each is constructed as a CheckedPanel with a kernel-checked Boolean validity field. The objects certify only the original finite arithmetic conditions; the analytic integral error bound is a separate theorem.
Port note. This is a port, to the Mathlib 777aaa6 / Lean v4.29.0-rc3 environment of the Riemann Hypothesis mission tree, of the definition TaoFivePrimes_RH14To100CheckedMomentNCPanels0 (id dfd3e590-3615-4a4f-bbf8-f7eab3896b9b, env 0df444a, published by @raresbuhai). The Lean source is unchanged.
Definition code
/- Proof-bearing finite certificate data from sometik179's original height-14–100 certificate; theta/Mellin attribution to Gabewhigham. The Boolean validity proof is a necessary constructor field, checked by the Lean kernel. -/ import Definitions.Def_TaoFivePrimes_RH14To100MomentCertificateDataNC set_option autoImplicit false set_option maxHeartbeats 0 set_option maxRecDepth 100000 set_option exponentiation.threshold 20000 set_option Elab.async false namespace RH14MomentCertificateData open RH14MomentEnclosureProof.CertifiedMomentRecords noncomputable def panel0 : CheckedPanel (0 : Fin 16) := ⟨panelAt 0, sequenceCacheAt 0, by decide +kernel⟩ noncomputable def panel1 : CheckedPanel (1 : Fin 16) := ⟨panelAt 1, sequenceCacheAt 1, by decide +kernel⟩ noncomputable def panel2 : CheckedPanel (2 : Fin 16) := ⟨panelAt 2, sequenceCacheAt 2, by decide +kernel⟩ noncomputable def panel3 : CheckedPanel (3 : Fin 16) := ⟨panelAt 3, sequenceCacheAt 3, by decide +kernel⟩ end RH14MomentCertificateData def TaoFivePrimes_RH14To100CheckedMomentNCPanels0 : Nat := 14
Source
sometik179, original height-14–100 certificate c9908072-d99a-4431-aad8-a72c6352619a (2026-10-03), https://prove2.me/submissions/c9908072-d99a-4431-aad8-a72c6352619a; original theta/Mellin foundations attributed to Gabewhigham. These same ordinary data and Boolean kernel validations occur in public moment-enclosure submission 821c0bfb-a758-4f7c-8bd3-e2b55ae05d26. The packet constructor validity proofs are necessary fields of dependent data structures; the substantive analytic enclosure remains a separate theorem.; ported from 0df444a definition dfd3e590-3615-4a4f-bbf8-f7eab3896b9b