RH height 14–100 — certified moment data panels2
DefinitionTaoFivePrimes_RH14To100CheckedMomentNCPanels2numerical-verificationriemann-zetatao-five-primes
Four proposed moment-certificate data records, for panel indices 8 through 11. 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_RH14To100CheckedMomentNCPanels2 (id 3fdca105-605c-46d2-8b90-9338f6ae9ac0, 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 panel8 : CheckedPanel (8 : Fin 16) := ⟨panelAt 8, sequenceCacheAt 8, by decide +kernel⟩ noncomputable def panel9 : CheckedPanel (9 : Fin 16) := ⟨panelAt 9, sequenceCacheAt 9, by decide +kernel⟩ noncomputable def panel10 : CheckedPanel (10 : Fin 16) := ⟨panelAt 10, sequenceCacheAt 10, by decide +kernel⟩ noncomputable def panel11 : CheckedPanel (11 : Fin 16) := ⟨panelAt 11, sequenceCacheAt 11, by decide +kernel⟩ end RH14MomentCertificateData def TaoFivePrimes_RH14To100CheckedMomentNCPanels2 : 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 3fdca105-605c-46d2-8b90-9338f6ae9ac0