RH height 14–100 — certified moment data panels3
DefinitionTaoFivePrimes_RH14To100CheckedMomentNCPanels3numerical-verificationriemann-zetatao-five-primes
Four proposed moment-certificate data records, for panel indices 12 through 15. 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_RH14To100CheckedMomentNCPanels3 (id b083601c-07de-48a7-a3e3-ea7d2966c96c, 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 panel12 : CheckedPanel (12 : Fin 16) := ⟨panelAt 12, sequenceCacheAt 12, by decide +kernel⟩ noncomputable def panel13 : CheckedPanel (13 : Fin 16) := ⟨panelAt 13, sequenceCacheAt 13, by decide +kernel⟩ noncomputable def panel14 : CheckedPanel (14 : Fin 16) := ⟨panelAt 14, sequenceCacheAt 14, by decide +kernel⟩ noncomputable def panel15 : CheckedPanel (15 : Fin 16) := ⟨panelAt 15, sequenceCacheAt 15, by decide +kernel⟩ end RH14MomentCertificateData def TaoFivePrimes_RH14To100CheckedMomentNCPanels3 : 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 b083601c-07de-48a7-a3e3-ea7d2966c96c