certificate, block 8
OpenThetaCert.run_8The kernel checker ThetaSieve.Seg.ok accepts every record of ThetaSieve.ThetaRun8.segs (block 8 of 102): for each segment, every window passes the two mesh checks and in fixed point, and the bounds for advance from the stated start values to the stated end values.
The blocks chain from to beyond ; with the soundness of the checker they give on that range.
Retired (2026-10-17) Superseded: this mesh block is not used, because the full mesh of the Chebyshev certificate exceeds the platform's per-job memory and time limits. The full Chebyshev certificate and its proof Dusart.chebyshev_theta_k2_finite are in the release doi:10.5281/zenodo.23432990; the checker and base range on this platform remain ThetaCertCore, ThetaCertData_base and ThetaCert.base.
import Definitions.Def_ThetaCertData_8
theorem ThetaCert.run_8 :
∀ s ∈ ThetaSieve.ThetaRun8.segs, s.ok = true := by sorry