Theta certificate data, block 22

Definition

ThetaCertData_22

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

analytic-number-theorynumber-theoryprime-numbers

Certificate records, block 22 of 102, 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.run_22 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 ThetaRun22.s0 : Seg := ⟨13866283717169611721923456303, 13866370160999251705813011770, 751732441, 1048576, [45882, 45887, 45893, 45898, 45904, 45910, 45915, 45921, 45926, 45932, 45938, 45943, 45949, 45954, 45960, 45966, 45971, 45977, 45983, 45988, 45994, 45999, 37886], 13904941329188349810725549129, 13905028002418917015599937001⟩
def ThetaRun22.s1 : Seg := ⟨13904941329188349810725549129, 13905028002418917015599937001, 753829593, 1048576, [46010, 46015, 46021, 46026, 46032, 46038, 46043, 46049, 46055, 46060, 46066, 46071, 46077, 46083, 46088, 46094, 46100, 46105, 46111, 46116, 46122, 46128, 35066], 13943740343027247581904762974, 13943827246080612535981362356⟩
def ThetaRun22.s2 : Seg := ⟨13943740343027247581904762974, 13943827246080612535981362356, 755926745, 1048576, [46138, 46143, 46149, 46155, 46160, 46166, 46171, 46177, 46183, 46188, 46194, 46200, 46205, 46211, 46217, 46222, 46228, 46233, 46239, 46245, 46250, 46256, 32246], 13982406205914945623251344625, 13982493337639354960858823791⟩
def ThetaRun22.s3 : Seg := ⟨13982406205914945623251344625, 13982493337639354960858823791, 758023897, 1048576, [46266, 46271, 46277, 46283, 46288, 46294, 46300, 46305, 46311, 46316, 46322, 46328, 46333, 46339, 46345, 46350, 46356, 46362, 46367, 46373, 46379, 46384, 29427], 14021043738454904840391251400, 14021131098429213781642602318⟩
def ThetaRun22.s4 : Seg := ⟨14021043738454904840391251400, 14021131098429213781642602318, 760121049, 1048576, [46394, 46399, 46405, 46411, 46416, 46422, 46428, 46433, 46439, 46445, 46450, 46456, 46462, 46467, 46473, 46479, 46484, 46490, 46496, 46501, 46507, 46513, 26606], 14059764194431023317381019053, 14059851782938851355935089214⟩
def ThetaRun22.s5 : Seg := ⟨14059764194431023317381019053, 14059851782938851355935089214, 762218201, 1048576, [46522, 46527, 46533, 46539, 46544, 46550, 46556, 46561, 46567, 46573, 46578, 46584, 46590, 46595, 46601, 46607, 46613, 46618, 46624, 46630, 46635, 46641, 23788], 14098378173842175563200576413, 14098465990154637295869746176⟩
def ThetaRun22.s6 : Seg := ⟨14098378173842175563200576413, 14098465990154637295869746176, 764315353, 1048576, [46650, 46655, 46661, 46667, 46672, 46678, 46684, 46689, 46695, 46701, 46707, 46712, 46718, 46724, 46729, 46735, 46741, 46747, 46752, 46758, 46764, 46769, 20968], 14136932812523825146918698446, 14137020856370942787246836627⟩
def ThetaRun22.s7 : Seg := ⟨14136932812523825146918698446, 14137020856370942787246836627, 766412505, 1048576, [46778, 46783, 46789, 46795, 46800, 46806, 46812, 46818, 46823, 46829, 46835, 46840, 46846, 46852, 46858, 46863, 46869, 46875, 46880, 46886, 46892, 46898, 18149], 14175662433841465930281173994, 14175750706306352716696582491⟩
def ThetaRun22.s8 : Seg := ⟨14175662433841465930281173994, 14175750706306352716696582491, 768509657, 1048576, [46906, 46911, 46917, 46923, 46929, 46934, 46940, 46946, 46951, 46957, 46963, 46969, 46974, 46980, 46986, 46992, 46997, 47003, 47009, 47015, 47020, 47026, 15328], 14214426659980757391092863896, 14214515161401761788562513883⟩
def ThetaRun22.s9 : Seg := ⟨14214426659980757391092863896, 14214515161401761788562513883, 770606809, 1048576, [47034, 47039, 47045, 47051, 47057, 47062, 47068, 47074, 47080, 47085, 47091, 47097, 47103, 47108, 47114, 47120, 47126, 47131, 47137, 47143, 47149, 47154, 12508], 14253187362535176959741949432, 14253276093167150580937573110⟩
def ThetaRun22.s10 : Seg := ⟨14253187362535176959741949432, 14253276093167150580937573110, 772703961, 1048576, [47162, 47167, 47173, 47179, 47185, 47190, 47196, 47202, 47208, 47213, 47219, 47225, 47231, 47237, 47242, 47248, 47254, 47260, 47265, 47271, 47277, 47283, 9689], 14291778780390103367592625299, 14291867739489744499845249116⟩
def ThetaRun22.s11 : Seg := ⟨14291778780390103367592625299, 14291867739489744499845249116, 774801113, 1048576, [47290, 47295, 47301, 47307, 47313, 47318, 47324, 47330, 47336, 47342, 47347, 47353, 47359, 47365, 47370, 47376, 47382, 47388, 47394, 47399, 47405, 47411, 6871], 14330421362492169839231938166, 14330510550735923454352392135⟩
def ThetaRun22.s12 : Seg := ⟨14330421362492169839231938166, 14330510550735923454352392135, 776898265, 1048576, [47418, 47423, 47429, 47435, 47441, 47447, 47452, 47458, 47464, 47470, 47476, 47481, 47487, 47493, 47499, 47505, 47510, 47516, 47522, 47528, 47534, 47539, 4049], 14369121910553736946183720791, 14369211328738080382761980894⟩
def ThetaRun22.s13 : Seg := ⟨14369121910553736946183720791, 14369211328738080382761980894, 778995417, 1048576, [47546, 47551, 47557, 47563, 47569, 47575, 47580, 47586, 47592, 47598, 47604, 47609, 47615, 47621, 47627, 47633, 47639, 47644, 47650, 47656, 47662, 47668, 1231], 14407804133958670494858610188, 14407893782490230979975200586⟩
def ThetaRun22.s14 : Seg := ⟨14407804133958670494858610188, 14407893782490230979975200586, 781092569, 1048576, [47674, 47679, 47685, 47691, 47697, 47703, 47709, 47714, 47720, 47726, 47732, 47738, 47743, 47749, 47755, 47761, 47767, 47773, 47778, 47784, 47790, 46208], 14446563955959472487564557260, 14446653835192717765007166926⟩
def ThetaRun22.s15 : Seg := ⟨14446563955959472487564557260, 14446653835192717765007166926, 783189721, 1048576, [47802, 47807, 47813, 47819, 47825, 47831, 47837, 47842, 47848, 47854, 47860, 47866, 47872, 47878, 47883, 47889, 47895, 47901, 47907, 47913, 47918, 43516], 14485315248061900192869166355, 14485405357357790929986204465⟩
def ThetaRun22.s16 : Seg := ⟨14485315248061900192869166355, 14485405357357790929986204465, 785286873, 1048576, [47930, 47935, 47941, 47947, 47953, 47959, 47965, 47971, 47976, 47982, 47988, 47994, 48000, 48006, 48012, 48017, 48023, 48029, 48035, 48041, 48047, 40825], 14523991866285708586720591448, 14524082204724751157258254704⟩

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

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