Theta certificate data, block 7

Definition
ThetaCertData_7
by @bwdaugherty · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)
analytic-number-theorynumber-theoryprime-numbers
Certificate records, block 7 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_7 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 ThetaRun7.s0 : Seg := ⟨4001841733681926712131771836, 4001868062150770228487153761, 216958681, 1048576, [13242, 13243, 13245, 13246, 13248, 13250, 13251, 13253, 13255, 13256, 13258, 13259, 13261, 13263, 13264, 13266, 13267, 13269, 13271, 13272, 13274, 13276, 13277, 13279, 13280, 13282, 13284, 13285, 13287, 13289, 13290, 13292, 13293, 13295, 13297, 13298, 13300, 13302, 13303, 13305, 13306, 13308, 13310, 13311, 13313, 13315, 13316, 13318, 13319, 13321, 13323, 13324, 13326, 13328, 13329, 13331, 13332, 13334, 13336, 13337, 13339, 13341, 13342, 13344, 13345, 13347, 13349, 13350, 13352, 13354, 13355, 13357, 13358, 13360, 13362, 13363, 13365, 13367, 10862], 4040507945782825331265349394, 4040534519577930803640277509⟩
def ThetaRun7.s1 : Seg := ⟨4040507945782825331265349394, 4040534519577930803640277509, 219055833, 1048576, [13370, 13371, 13373, 13375, 13376, 13378, 13379, 13381, 13383, 13384, 13386, 13388, 13389, 13391, 13392, 13394, 13396, 13397, 13399, 13401, 13402, 13404, 13406, 13407, 13409, 13410, 13412, 13414, 13415, 13417, 13419, 13420, 13422, 13424, 13425, 13427, 13428, 13430, 13432, 13433, 13435, 13437, 13438, 13440, 13442, 13443, 13445, 13447, 13448, 13450, 13451, 13453, 13455, 13456, 13458, 13460, 13461, 13463, 13465, 13466, 13468, 13470, 13471, 13473, 13474, 13476, 13478, 13479, 13481, 13483, 13484, 13486, 13488, 13489, 13491, 13493, 13494, 13496, 830], 4079144539403033685296790713, 4079171358519362225639975209⟩
def ThetaRun7.s2 : Seg := ⟨4079144539403033685296790713, 4079171358519362225639975209, 221152985, 1048576, [13498, 13499, 13501, 13503, 13504, 13506, 13507, 13509, 13511, 13512, 13514, 13516, 13517, 13519, 13521, 13522, 13524, 13526, 13527, 13529, 13531, 13532, 13534, 13536, 13537, 13539, 13541, 13542, 13544, 13545, 13547, 13549, 13550, 13552, 13554, 13555, 13557, 13559, 13560, 13562, 13564, 13565, 13567, 13569, 13570, 13572, 13574, 13575, 13577, 13579, 13580, 13582, 13584, 13585, 13587, 13589, 13590, 13592, 13594, 13595, 13597, 13598, 13600, 13602, 13603, 13605, 13607, 13608, 13610, 13612, 13613, 13615, 13617, 13618, 13620, 13622, 13623, 4425], 4117899477739489373758101768, 4117926542309831636067497833⟩
def ThetaRun7.s3 : Seg := ⟨4117899477739489373758101768, 4117926542309831636067497833, 223250137, 1048576, [13626, 13627, 13629, 13631, 13632, 13634, 13636, 13637, 13639, 13641, 13642, 13644, 13646, 13647, 13649, 13651, 13652, 13654, 13656, 13657, 13659, 13661, 13662, 13664, 13666, 13667, 13669, 13671, 13672, 13674, 13676, 13677, 13679, 13681, 13682, 13684, 13686, 13687, 13689, 13691, 13692, 13694, 13696, 13697, 13699, 13701, 13702, 13704, 13706, 13707, 13709, 13711, 13712, 13714, 13716, 13717, 13719, 13721, 13722, 13724, 13726, 13727, 13729, 13731, 13732, 13734, 13736, 13737, 13739, 13741, 13743, 13744, 13746, 13748, 13749, 13751, 8273], 4156574731050614333889227668, 4156602040372095162085991576⟩
def ThetaRun7.s4 : Seg := ⟨4156574731050614333889227668, 4156602040372095162085991576, 225347289, 1048576, [13754, 13755, 13757, 13759, 13760, 13762, 13764, 13765, 13767, 13769, 13770, 13772, 13774, 13775, 13777, 13779, 13780, 13782, 13784, 13786, 13787, 13789, 13791, 13792, 13794, 13796, 13797, 13799, 13801, 13802, 13804, 13806, 13807, 13809, 13811, 13812, 13814, 13816, 13818, 13819, 13821, 13823, 13824, 13826, 13828, 13829, 13831, 13833, 13834, 13836, 13838, 13839, 13841, 13843, 13845, 13846, 13848, 13850, 13851, 13853, 13855, 13856, 13858, 13860, 13861, 13863, 13865, 13867, 13868, 13870, 13872, 13873, 13875, 13877, 13878, 12384], 4195284337204218801305011623, 4195311891817198691400428564⟩
def ThetaRun7.s5 : Seg := ⟨4195284337204218801305011623, 4195311891817198691400428564, 227444441, 1048576, [13882, 13883, 13885, 13887, 13888, 13890, 13892, 13893, 13895, 13897, 13899, 13900, 13902, 13904, 13905, 13907, 13909, 13910, 13912, 13914, 13916, 13917, 13919, 13921, 13922, 13924, 13926, 13927, 13929, 13931, 13933, 13934, 13936, 13938, 13939, 13941, 13943, 13944, 13946, 13948, 13950, 13951, 13953, 13955, 13956, 13958, 13960, 13961, 13963, 13965, 13967, 13968, 13970, 13972, 13973, 13975, 13977, 13979, 13980, 13982, 13984, 13985, 13987, 13989, 13990, 13992, 13994, 13996, 13997, 13999, 14001, 14002, 14004, 14006, 14008, 2739], 4233895334260339007316794616, 4233923133213000518627838862⟩
def ThetaRun7.s6 : Seg := ⟨4233895334260339007316794616, 4233923133213000518627838862, 229541593, 1048576, [14010, 14011, 14013, 14015, 14016, 14018, 14020, 14022, 14023, 14025, 14027, 14028, 14030, 14032, 14034, 14035, 14037, 14039, 14040, 14042, 14044, 14046, 14047, 14049, 14051, 14052, 14054, 14056, 14058, 14059, 14061, 14063, 14064, 14066, 14068, 14070, 14071, 14073, 14075, 14076, 14078, 14080, 14082, 14083, 14085, 14087, 14088, 14090, 14092, 14094, 14095, 14097, 14099, 14101, 14102, 14104, 14106, 14107, 14109, 14111, 14113, 14114, 14116, 14118, 14119, 14121, 14123, 14125, 14126, 14128, 14130, 14132, 14133, 14135, 7233], 4272671355638076438177892741, 4272699399505953335197927572⟩
def ThetaRun7.s7 : Seg := ⟨4272671355638076438177892741, 4272699399505953335197927572, 231638745, 1048576, [14138, 14139, 14141, 14143, 14145, 14146, 14148, 14150, 14151, 14153, 14155, 14157, 14158, 14160, 14162, 14164, 14165, 14167, 14169, 14170, 14172, 14174, 14176, 14177, 14179, 14181, 14183, 14184, 14186, 14188, 14189, 14191, 14193, 14195, 14196, 14198, 14200, 14202, 14203, 14205, 14207, 14209, 14210, 14212, 14214, 14215, 14217, 14219, 14221, 14222, 14224, 14226, 14228, 14229, 14231, 14233, 14235, 14236, 14238, 14240, 14242, 14243, 14245, 14247, 14248, 14250, 14252, 14254, 14255, 14257, 14259, 14261, 14262, 11982], 4311258418685549487711923145, 4311286706586944303384357833⟩
def ThetaRun7.s8 : Seg := ⟨4311258418685549487711923145, 4311286706586944303384357833, 233735897, 1048576, [14266, 14267, 14269, 14271, 14273, 14274, 14276, 14278, 14280, 14281, 14283, 14285, 14287, 14288, 14290, 14292, 14293, 14295, 14297, 14299, 14300, 14302, 14304, 14306, 14307, 14309, 14311, 14313, 14314, 14316, 14318, 14320, 14321, 14323, 14325, 14327, 14328, 14330, 14332, 14334, 14335, 14337, 14339, 14341, 14342, 14344, 14346, 14348, 14349, 14351, 14353, 14355, 14356, 14358, 14360, 14362, 14363, 14365, 14367, 14369, 14370, 14372, 14374, 14376, 14377, 14379, 14381, 14383, 14385, 14386, 14388, 14390, 14392, 2599], 4349945945472139058540961403, 4349974477890874563350837128⟩
def ThetaRun7.s9 : Seg := ⟨4349945945472139058540961403, 4349974477890874563350837128, 235833049, 1048576, [14394, 14395, 14397, 14399, 14401, 14402, 14404, 14406, 14408, 14409, 14411, 14413, 14415, 14416, 14418, 14420, 14422, 14424, 14425, 14427, 14429, 14431, 14432, 14434, 14436, 14438, 14439, 14441, 14443, 14445, 14446, 14448, 14450, 14452, 14453, 14455, 14457, 14459, 14461, 14462, 14464, 14466, 14468, 14469, 14471, 14473, 14475, 14476, 14478, 14480, 14482, 14483, 14485, 14487, 14489, 14491, 14492, 14494, 14496, 14498, 14499, 14501, 14503, 14505, 14506, 14508, 14510, 14512, 14514, 14515, 14517, 14519, 7733], 4388723883453483437102817858, 4388752660475194783301340863⟩
def ThetaRun7.s10 : Seg := ⟨4388723883453483437102817858, 4388752660475194783301340863, 237930201, 1048576, [14522, 14523, 14525, 14527, 14529, 14530, 14532, 14534, 14536, 14538, 14539, 14541, 14543, 14545, 14546, 14548, 14550, 14552, 14554, 14555, 14557, 14559, 14561, 14562, 14564, 14566, 14568, 14570, 14571, 14573, 14575, 14577, 14578, 14580, 14582, 14584, 14586, 14587, 14589, 14591, 14593, 14594, 14596, 14598, 14600, 14602, 14603, 14605, 14607, 14609, 14611, 14612, 14614, 14616, 14618, 14619, 14621, 14623, 14625, 14627, 14628, 14630, 14632, 14634, 14635, 14637, 14639, 14641, 14643, 14644, 14646, 13125], 4427428434956573405418454147, 4427457456536353663678256740⟩
def ThetaRun7.s11 : Seg := ⟨4427428434956573405418454147, 4427457456536353663678256740, 240027353, 1048576, [14650, 14651, 14653, 14655, 14657, 14659, 14660, 14662, 14664, 14666, 14667, 14669, 14671, 14673, 14675, 14676, 14678, 14680, 14682, 14684, 14685, 14687, 14689, 14691, 14693, 14694, 14696, 14698, 14700, 14702, 14703, 14705, 14707, 14709, 14711, 14712, 14714, 14716, 14718, 14720, 14721, 14723, 14725, 14727, 14728, 14730, 14732, 14734, 14736, 14737, 14739, 14741, 14743, 14745, 14746, 14748, 14750, 14752, 14754, 14755, 14757, 14759, 14761, 14763, 14764, 14766, 14768, 14770, 14772, 14774, 14775, 3999], 4466139116639877523069327432, 4466168382323593408991206063⟩
def ThetaRun7.s12 : Seg := ⟨4466139116639877523069327432, 4466168382323593408991206063, 242124505, 1048576, [14778, 14779, 14781, 14783, 14785, 14787, 14788, 14790, 14792, 14794, 14796, 14797, 14799, 14801, 14803, 14805, 14806, 14808, 14810, 14812, 14814, 14816, 14817, 14819, 14821, 14823, 14825, 14826, 14828, 14830, 14832, 14834, 14835, 14837, 14839, 14841, 14843, 14844, 14846, 14848, 14850, 14852, 14854, 14855, 14857, 14859, 14861, 14863, 14864, 14866, 14868, 14870, 14872, 14874, 14875, 14877, 14879, 14881, 14883, 14884, 14886, 14888, 14890, 14892, 14894, 14895, 14897, 14899, 14901, 14903, 9775], 4504746799805612667119995258, 4504776308737586200856012553⟩
def ThetaRun7.s13 : Seg := ⟨4504746799805612667119995258, 4504776308737586200856012553, 244221657, 1048576, [14906, 14907, 14909, 14911, 14913, 14915, 14917, 14918, 14920, 14922, 14924, 14926, 14927, 14929, 14931, 14933, 14935, 14937, 14938, 14940, 14942, 14944, 14946, 14948, 14949, 14951, 14953, 14955, 14957, 14958, 14960, 14962, 14964, 14966, 14968, 14969, 14971, 14973, 14975, 14977, 14979, 14980, 14982, 14984, 14986, 14988, 14990, 14991, 14993, 14995, 14997, 14999, 15001, 15002, 15004, 15006, 15008, 15010, 15012, 15013, 15015, 15017, 15019, 15021, 15023, 15024, 15026, 15028, 15030, 15032, 775], 4543474613457334882137820364, 4543504366910644271868586404⟩
def ThetaRun7.s14 : Seg := ⟨4543474613457334882137820364, 4543504366910644271868586404, 246318809, 1048576, [15034, 15035, 15037, 15039, 15041, 15043, 15045, 15046, 15048, 15050, 15052, 15054, 15056, 15057, 15059, 15061, 15063, 15065, 15067, 15069, 15070, 15072, 15074, 15076, 15078, 15080, 15081, 15083, 15085, 15087, 15089, 15091, 15092, 15094, 15096, 15098, 15100, 15102, 15104, 15105, 15107, 15109, 15111, 15113, 15115, 15116, 15118, 15120, 15122, 15124, 15126, 15127, 15129, 15131, 15133, 15135, 15137, 15139, 15140, 15142, 15144, 15146, 15148, 15150, 15152, 15153, 15155, 15157, 15159, 6940], 4582187430580769897396561582, 4582217427677168075290348243⟩
def ThetaRun7.s15 : Seg := ⟨4582187430580769897396561582, 4582217427677168075290348243, 248415961, 1048576, [15162, 15163, 15165, 15167, 15169, 15171, 15173, 15175, 15176, 15178, 15180, 15182, 15184, 15186, 15188, 15189, 15191, 15193, 15195, 15197, 15199, 15201, 15202, 15204, 15206, 15208, 15210, 15212, 15214, 15215, 15217, 15219, 15221, 15223, 15225, 15227, 15228, 15230, 15232, 15234, 15236, 15238, 15240, 15241, 15243, 15245, 15247, 15249, 15251, 15253, 15254, 15256, 15258, 15260, 15262, 15264, 15266, 15267, 15269, 15271, 15273, 15275, 15277, 15279, 15281, 15282, 15284, 15286, 13358], 4620867934144759201239082683, 4620898175028847188657769427⟩
def ThetaRun7.s16 : Seg := ⟨4620867934144759201239082683, 4620898175028847188657769427, 250513113, 1048576, [15290, 15291, 15293, 15295, 15297, 15299, 15301, 15303, 15305, 15306, 15308, 15310, 15312, 15314, 15316, 15318, 15319, 15321, 15323, 15325, 15327, 15329, 15331, 15333, 15334, 15336, 15338, 15340, 15342, 15344, 15346, 15348, 15349, 15351, 15353, 15355, 15357, 15359, 15361, 15363, 15364, 15366, 15368, 15370, 15372, 15374, 15376, 15378, 15379, 15381, 15383, 15385, 15387, 15389, 15391, 15393, 15394, 15396, 15398, 15400, 15402, 15404, 15406, 15408, 15410, 15411, 15413, 15415, 4621], 4659568040436641427963731241, 4659598524762391814059022623⟩

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