Theta certificate data, block 10

Definition

ThetaCertData_10

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

analytic-number-theorynumber-theoryprime-numbers

Certificate records, block 10 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_10 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 ThetaRun10.s0 : Seg := ⟨5974764021774186286816777572, 5974802725604360969356843745, 323913433, 1048576, [19770, 19772, 19774, 19777, 19779, 19782, 19784, 19787, 19789, 19791, 19794, 19796, 19799, 19801, 19803, 19806, 19808, 19811, 19813, 19816, 19818, 19820, 19823, 19825, 19828, 19830, 19832, 19835, 19837, 19840, 19842, 19845, 19847, 19849, 19852, 19854, 19857, 19859, 19862, 19864, 19866, 19869, 19871, 19874, 19876, 19878, 19881, 19883, 19886, 19888, 19891, 19893, 17349], 6013436938164245173856488792, 6013475882342716792404650523⟩
def ThetaRun10.s1 : Seg := ⟨6013436938164245173856488792, 6013475882342716792404650523, 326010585, 1048576, [19898, 19900, 19902, 19905, 19907, 19910, 19912, 19915, 19917, 19919, 19922, 19924, 19927, 19929, 19932, 19934, 19937, 19939, 19941, 19944, 19946, 19949, 19951, 19954, 19956, 19958, 19961, 19963, 19966, 19968, 19971, 19973, 19975, 19978, 19980, 19983, 19985, 19988, 19990, 19993, 19995, 19997, 20000, 20002, 20005, 20007, 20010, 20012, 20015, 20017, 20019, 20022, 10673], 6052159433824995617661491773, 6052198617912520808593927219⟩
def ThetaRun10.s2 : Seg := ⟨6052159433824995617661491773, 6052198617912520808593927219, 328107737, 1048576, [20026, 20028, 20030, 20033, 20035, 20038, 20040, 20043, 20045, 20048, 20050, 20053, 20055, 20057, 20060, 20062, 20065, 20067, 20070, 20072, 20075, 20077, 20079, 20082, 20084, 20087, 20089, 20092, 20094, 20097, 20099, 20102, 20104, 20106, 20109, 20111, 20114, 20116, 20119, 20121, 20124, 20126, 20129, 20131, 20133, 20136, 20138, 20141, 20143, 20146, 20148, 20151, 3996], 6090809177478029828329610294, 6090848601371402313729423796⟩
def ThetaRun10.s3 : Seg := ⟨6090809177478029828329610294, 6090848601371402313729423796, 330204889, 1048576, [20154, 20156, 20159, 20161, 20163, 20166, 20168, 20171, 20173, 20176, 20178, 20181, 20183, 20186, 20188, 20191, 20193, 20195, 20198, 20200, 20203, 20205, 20208, 20210, 20213, 20215, 20218, 20220, 20223, 20225, 20228, 20230, 20232, 20235, 20237, 20240, 20242, 20245, 20247, 20250, 20252, 20255, 20257, 20260, 20262, 20265, 20267, 20270, 20272, 20275, 20277, 17598], 6129437421651141603317673905, 6129477085344323300220242041⟩
def ThetaRun10.s4 : Seg := ⟨6129437421651141603317673905, 6129477085344323300220242041, 332302041, 1048576, [20282, 20284, 20287, 20289, 20292, 20294, 20296, 20299, 20301, 20304, 20306, 20309, 20311, 20314, 20316, 20319, 20321, 20324, 20326, 20329, 20331, 20334, 20336, 20339, 20341, 20344, 20346, 20349, 20351, 20354, 20356, 20358, 20361, 20363, 20366, 20368, 20371, 20373, 20376, 20378, 20381, 20383, 20386, 20388, 20391, 20393, 20396, 20398, 20401, 20403, 20406, 11052], 6168129125781858030820721462, 6168169028969461227576561544⟩
def ThetaRun10.s5 : Seg := ⟨6168129125781858030820721462, 6168169028969461227576561544, 334399193, 1048576, [20410, 20412, 20415, 20417, 20420, 20422, 20425, 20427, 20430, 20432, 20435, 20437, 20440, 20442, 20445, 20447, 20450, 20452, 20454, 20457, 20459, 20462, 20464, 20467, 20469, 20472, 20474, 20477, 20479, 20482, 20484, 20487, 20489, 20492, 20494, 20497, 20499, 20502, 20504, 20507, 20510, 20512, 20515, 20517, 20520, 20522, 20525, 20527, 20530, 20532, 20535, 4502], 6206842972860125734220125373, 6206883115934332296890822572⟩
def ThetaRun10.s6 : Seg := ⟨6206842972860125734220125373, 6206883115934332296890822572, 336496345, 1048576, [20538, 20540, 20543, 20545, 20548, 20550, 20553, 20555, 20558, 20560, 20563, 20565, 20568, 20570, 20573, 20575, 20578, 20580, 20583, 20585, 20588, 20590, 20593, 20595, 20598, 20600, 20603, 20605, 20608, 20610, 20613, 20615, 20618, 20621, 20623, 20626, 20628, 20631, 20633, 20636, 20638, 20641, 20643, 20646, 20648, 20651, 20653, 20656, 20658, 20661, 18617], 6245484717459176939463214548, 6245525100292961773036919165⟩
def ThetaRun10.s7 : Seg := ⟨6245484717459176939463214548, 6245525100292961773036919165, 338593497, 1048576, [20666, 20668, 20671, 20673, 20676, 20678, 20681, 20683, 20686, 20688, 20691, 20693, 20696, 20698, 20701, 20703, 20706, 20709, 20711, 20714, 20716, 20719, 20721, 20724, 20726, 20729, 20731, 20734, 20736, 20739, 20741, 20744, 20746, 20749, 20752, 20754, 20757, 20759, 20762, 20764, 20767, 20769, 20772, 20774, 20777, 20779, 20782, 20785, 20787, 20790, 12199], 6284206408274775465240860101, 6284247030605753723818982628⟩
def ThetaRun10.s8 : Seg := ⟨6284206408274775465240860101, 6284247030605753723818982628, 340690649, 1048576, [20794, 20796, 20799, 20801, 20804, 20806, 20809, 20811, 20814, 20816, 20819, 20822, 20824, 20827, 20829, 20832, 20834, 20837, 20839, 20842, 20844, 20847, 20850, 20852, 20855, 20857, 20860, 20862, 20865, 20867, 20870, 20872, 20875, 20878, 20880, 20883, 20885, 20888, 20890, 20893, 20895, 20898, 20900, 20903, 20906, 20908, 20911, 20913, 20916, 20918, 5780], 6322907241262103965380703712, 6322948103014747041057878934⟩
def ThetaRun10.s9 : Seg := ⟨6322907241262103965380703712, 6322948103014747041057878934, 342787801, 1048576, [20922, 20924, 20927, 20929, 20932, 20934, 20937, 20939, 20942, 20945, 20947, 20950, 20952, 20955, 20957, 20960, 20963, 20965, 20968, 20970, 20973, 20975, 20978, 20980, 20983, 20986, 20988, 20991, 20993, 20996, 20998, 21001, 21003, 21006, 21009, 21011, 21014, 21016, 21019, 21021, 21024, 21027, 21029, 21032, 21034, 21037, 21039, 21042, 21045, 20408], 6361633906399205782482096707, 6361675008498807047064497080⟩
def ThetaRun10.s10 : Seg := ⟨6361633906399205782482096707, 6361675008498807047064497080, 344884953, 1048576, [21050, 21052, 21055, 21057, 21060, 21062, 21065, 21068, 21070, 21073, 21075, 21078, 21080, 21083, 21086, 21088, 21091, 21093, 21096, 21098, 21101, 21104, 21106, 21109, 21111, 21114, 21117, 21119, 21122, 21124, 21127, 21129, 21132, 21135, 21137, 21140, 21142, 21145, 21147, 21150, 21153, 21155, 21158, 21160, 21163, 21166, 21168, 21171, 21173, 14118], 6400317063371455267029005884, 6400358404544742419491958609⟩
def ThetaRun10.s11 : Seg := ⟨6400317063371455267029005884, 6400358404544742419491958609, 346982105, 1048576, [21178, 21180, 21183, 21185, 21188, 21191, 21193, 21196, 21198, 21201, 21203, 21206, 21209, 21211, 21214, 21216, 21219, 21222, 21224, 21227, 21229, 21232, 21235, 21237, 21240, 21242, 21245, 21248, 21250, 21253, 21255, 21258, 21260, 21263, 21266, 21268, 21271, 21273, 21276, 21279, 21281, 21284, 21286, 21289, 21292, 21294, 21297, 21299, 21302, 7828], 6438899641331863981072526042, 6438941220828641275485822631⟩
def ThetaRun10.s12 : Seg := ⟨6438899641331863981072526042, 6438941220828641275485822631, 349079257, 1048576, [21306, 21308, 21311, 21313, 21316, 21319, 21321, 21324, 21326, 21329, 21332, 21334, 21337, 21339, 21342, 21345, 21347, 21350, 21352, 21355, 21358, 21360, 21363, 21366, 21368, 21371, 21373, 21376, 21379, 21381, 21384, 21386, 21389, 21392, 21394, 21397, 21399, 21402, 21405, 21407, 21410, 21412, 21415, 21418, 21420, 21423, 21426, 21428, 21431, 1537], 6477664565758350795896244239, 6477706385424282802710117254⟩
def ThetaRun10.s13 : Seg := ⟨6477664565758350795896244239, 6477706385424282802710117254, 351176409, 1048576, [21434, 21436, 21439, 21441, 21444, 21447, 21449, 21452, 21455, 21457, 21460, 21462, 21465, 21468, 21470, 21473, 21476, 21478, 21481, 21483, 21486, 21489, 21491, 21494, 21496, 21499, 21502, 21504, 21507, 21510, 21512, 21515, 21517, 21520, 21523, 21525, 21528, 21531, 21533, 21536, 21539, 21541, 21544, 21546, 21549, 21552, 21554, 21557, 16806], 6516338171943284302636487125, 6516380230620145720477299009⟩
def ThetaRun10.s14 : Seg := ⟨6516338171943284302636487125, 6516380230620145720477299009, 353273561, 1048576, [21562, 21564, 21567, 21570, 21572, 21575, 21577, 21580, 21583, 21585, 21588, 21591, 21593, 21596, 21598, 21601, 21604, 21606, 21609, 21612, 21614, 21617, 21620, 21622, 21625, 21628, 21630, 21633, 21635, 21638, 21641, 21643, 21646, 21649, 21651, 21654, 21657, 21659, 21662, 21664, 21667, 21670, 21672, 21675, 21678, 21680, 21683, 21686, 10644], 6555034697957837705641589116, 6555076995369291847837037030⟩
def ThetaRun10.s15 : Seg := ⟨6555034697957837705641589116, 6555076995369291847837037030, 355370713, 1048576, [21690, 21692, 21695, 21698, 21700, 21703, 21705, 21708, 21711, 21713, 21716, 21719, 21721, 21724, 21727, 21729, 21732, 21735, 21737, 21740, 21743, 21745, 21748, 21751, 21753, 21756, 21759, 21761, 21764, 21767, 21769, 21772, 21774, 21777, 21780, 21782, 21785, 21788, 21790, 21793, 21796, 21798, 21801, 21804, 21806, 21809, 21812, 21814, 4484], 6593704317144387081262612197, 6593746853385436227887582108⟩
def ThetaRun10.s16 : Seg := ⟨6593704317144387081262612197, 6593746853385436227887582108, 357467865, 1048576, [21818, 21820, 21823, 21826, 21828, 21831, 21834, 21836, 21839, 21842, 21844, 21847, 21850, 21852, 21855, 21858, 21860, 21863, 21866, 21868, 21871, 21874, 21876, 21879, 21882, 21884, 21887, 21890, 21892, 21895, 21898, 21900, 21903, 21906, 21908, 21911, 21914, 21916, 21919, 21922, 21924, 21927, 21930, 21932, 21935, 21938, 21940, 20263], 6632386913459139826346122861, 6632429689051493615425547943⟩

def ThetaRun10.segs : List Seg := [ThetaRun10.s0, ThetaRun10.s1, ThetaRun10.s2, ThetaRun10.s3, ThetaRun10.s4, ThetaRun10.s5, ThetaRun10.s6, ThetaRun10.s7, ThetaRun10.s8, ThetaRun10.s9, ThetaRun10.s10, ThetaRun10.s11, ThetaRun10.s12, ThetaRun10.s13, ThetaRun10.s14, ThetaRun10.s15, ThetaRun10.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