certificate, mesh block 219
OpenThetaCert.mesh_219The kernel checker ThetaSieve.Seg.ok accepts every record of ThetaSieve.ThetaMesh219.segs (mesh block 219 of 220): 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_ThetaMeshData_219
theorem ThetaCert.mesh_219 :
∀ s ∈ ThetaSieve.ThetaMesh219.segs, s.ok = true := by sorry