RH height 14–100 — bernstein certificate verification
ProvedTaoFivePrimes.rh14to100_bernstein_checksAll ninety-three integer Bernstein certificates for the existing height-14–100 pilot are valid. For each of the eighty-six height slabs and each of its at most two box specifications, the certificate agrees with the integer power matrix, both exact Bernstein transforms, and the required positive lower threshold.
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_bernstein_checks (id 48937c8a-7f9a-4d3b-a5ae-c7102f990bec, 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_RH14To100BernsteinInterface
theorem TaoFivePrimes.rh14to100_bernstein_checks : (∀ (i : Fin 86) (j : ℕ), j<(CertifiedLocalBoxes.rowSpecs i).length →
CertifiedStreamingLocalBoxes.valid i j (CertifiedStreamingLocalBoxes.certificateAt i j)) ∧
(∀ i : Fin 86, (CertifiedLocalBoxes.rowSpecs i).length≤ 2) := by sorry