Theta certificate mesh data, block 219

Definition

ThetaMeshData_219

by @bwdaugherty · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorynumber-theoryprime-numbers

Certificate records, mesh block 219 of 220, for $|\theta(t)-t|\le t/(5\log^2 t)$ on $[3594641, 3584912847]$ : each record is a segment of odd numbers, its split into windows, and fixed-point bounds for $Q\,\theta$ at its two ends ( $Q=2^{64}$ ).

The data are produced by a program and are checked, not trusted: the theorem ThetaCert.mesh_219 states that the kernel checker accepts every record.

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.

Definition code

import Definitions.Def_ThetaCertCore

namespace ThetaSieve
set_option maxRecDepth 100000

def ThetaMesh219.s0 : Seg := ⟨65869468720961703255390498928, 65869838477473277519417622126, 3570850193, 524288, [217947, 217974, 88367], 65888844456310982869664721467, 65889214309532132550616345319⟩
def ThetaMesh219.s1 : Seg := ⟨65888844456310982869664721467, 65889214309532132550616345319, 3571898769, 524288, [218011, 218038, 88239], 65908103995917910012676843040, 65908473945379921631806243639⟩
def ThetaMesh219.s2 : Seg := ⟨65908103995917910012676843040, 65908473945379921631806243639, 3572947345, 524288, [218075, 218102, 88111], 65927464422711081361239769072, 65927834468977208677817491032⟩
def ThetaMesh219.s3 : Seg := ⟨65927464422711081361239769072, 65927834468977208677817491032, 3573995921, 524288, [218139, 218166, 87983], 65946674160108114869194050391, 65947044302340256633360073978⟩
def ThetaMesh219.s4 : Seg := ⟨65946674160108114869194050391, 65947044302340256633360073978, 3575044497, 524288, [218203, 218230, 87855], 65966058232949448880471714653, 65966428471973211954760533122⟩
def ThetaMesh219.s5 : Seg := ⟨65966058232949448880471714653, 65966428471973211954760533122, 3576093073, 524288, [218267, 218294, 87727], 65985328944555674175160622866, 65985699279834296690411124380⟩
def ThetaMesh219.s6 : Seg := ⟨65985328944555674175160622866, 65985699279834296690411124380, 3577141649, 524288, [218331, 218358, 87599], 66004731388528198177488874347, 66005101820735501749367068366⟩
def ThetaMesh219.s7 : Seg := ⟨66004731388528198177488874347, 66005101820735501749367068366, 3578190225, 524288, [218395, 218422, 87471], 66024075250925290145052700073, 66024445779701924896665475508⟩
def ThetaMesh219.s8 : Seg := ⟨66024075250925290145052700073, 66024445779701924896665475508, 3579238801, 524288, [218459, 218486, 87343], 66043439661654002522384293346, 66043810286972875968969492827⟩
def ThetaMesh219.s9 : Seg := ⟨66043439661654002522384293346, 66043810286972875968969492827, 3580287377, 524288, [218523, 218550, 87215], 66062803111849140895069329868, 66063173833977605934832892691⟩
def ThetaMesh219.s10 : Seg := ⟨66062803111849140895069329868, 66063173833977605934832892691, 3581335953, 524288, [218587, 218614, 87087], 66082185487522638023341837312, 66082556306467851786187008483⟩
def ThetaMesh219.s11 : Seg := ⟨66082185487522638023341837312, 66082556306467851786187008483, 3582384529, 524288, [218651, 218678, 86959], 66101567715184230005645634225, 66101938630930069517669908194⟩
def ThetaMesh219.s12 : Seg := ⟨66101567715184230005645634225, 66101938630930069517669908194, 3583433105, 524288, [218715, 218742, 86831], 66120832917755836254605682528, 66121203929844109594207420685⟩
def ThetaMesh219.s13 : Seg := ⟨66120832917755836254605682528, 66121203929844109594207420685, 3584481681, 218779, [218779], 66128914945550189969955824543, 66129286002480237852280457430⟩

def ThetaMesh219.segs : List Seg := [ThetaMesh219.s0, ThetaMesh219.s1, ThetaMesh219.s2, ThetaMesh219.s3, ThetaMesh219.s4, ThetaMesh219.s5, ThetaMesh219.s6, ThetaMesh219.s7, ThetaMesh219.s8, ThetaMesh219.s9, ThetaMesh219.s10, ThetaMesh219.s11, ThetaMesh219.s12, ThetaMesh219.s13]

end ThetaSieve

Source

P. Dusart, Estimates of some functions over primes without R.H., arXiv:1002.0442 (2010), Theorem 5.2 (k = 2, η = 0.2, x ≥ 3 594 641); here the range [3 594 641, 3 584 912 847] is closed by a kernel-checked sieve certificate.

View graph