RH height 14–100 — theta certificate verification
ProvedTaoFivePrimes.rh14to100_theta_checksEvery active rounded theta-jet record in the existing height-14–100 pilot satisfies its finite integer validator. There are sixteen quadrature panels, at most eight theta terms per panel, and 184 jet entries per active term. The claim checks the input boxes, signed convolution products, carries, and successive jet bounds.
This finite certificate claim supports the existing height-14–100 pilot. Its predicates are the original ordinary Lean integer validators in the finite arithmetic interface.
Port note. Port to the Mathlib 777aaa6 / Lean v4.29.0-rc3 environment of the Riemann Hypothesis mission of the theorem TaoFivePrimes.rh14to100_theta_checks (id a832b809-21ef-4ab8-85da-4126226df31e, 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.
import Definitions.Def_TaoFivePrimes_RH14To100ThetaInterface
theorem TaoFivePrimes.rh14to100_theta_checks (i : Fin 16) (n : Fin 8) (ha : CertifiedThetaPoints.active i n) :
CertifiedJetRecords.checkRecord i n (CertifiedJetRecords.recordAt i n)=true := by sorry