Theta certificate data, block 9

Definition

ThetaCertData_9

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

analytic-number-theorynumber-theoryprime-numbers

Certificate records, block 9 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_9 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 ThetaRun9.s0 : Seg := ⟨5317086857365690478441380286, 5317121464834516731932589873, 288261849, 1048576, [17594, 17596, 17598, 17600, 17602, 17604, 17606, 17609, 17611, 17613, 17615, 17617, 17619, 17622, 17624, 17626, 17628, 17630, 17632, 17634, 17637, 17639, 17641, 17643, 17645, 17647, 17650, 17652, 17654, 17656, 17658, 17660, 17662, 17665, 17667, 17669, 17671, 17673, 17675, 17678, 17680, 17682, 17684, 17686, 17688, 17691, 17693, 17695, 17697, 17699, 17701, 17703, 17706, 17708, 17710, 17712, 17714, 17716, 17719, 6870], 5355800008769010330315192158, 5355834857813745646198709165⟩
def ThetaRun9.s1 : Seg := ⟨5355800008769010330315192158, 5355834857813745646198709165, 290359001, 1048576, [17722, 17724, 17726, 17728, 17730, 17732, 17735, 17737, 17739, 17741, 17743, 17745, 17748, 17750, 17752, 17754, 17756, 17758, 17761, 17763, 17765, 17767, 17769, 17771, 17774, 17776, 17778, 17780, 17782, 17784, 17787, 17789, 17791, 17793, 17795, 17797, 17800, 17802, 17804, 17806, 17808, 17811, 17813, 17815, 17817, 17819, 17821, 17824, 17826, 17828, 17830, 17832, 17834, 17837, 17839, 17841, 17843, 17845, 17139], 5394528246884265714877092290, 5394563338314929665424959700⟩
def ThetaRun9.s2 : Seg := ⟨5394528246884265714877092290, 5394563338314929665424959700, 292456153, 1048576, [17850, 17852, 17854, 17856, 17858, 17861, 17863, 17865, 17867, 17869, 17871, 17874, 17876, 17878, 17880, 17882, 17885, 17887, 17889, 17891, 17893, 17895, 17898, 17900, 17902, 17904, 17906, 17909, 17911, 17913, 17915, 17917, 17919, 17922, 17924, 17926, 17928, 17930, 17933, 17935, 17937, 17939, 17941, 17944, 17946, 17948, 17950, 17952, 17954, 17957, 17959, 17961, 17963, 17965, 17968, 17970, 17972, 17974, 9688], 5433248796121979959812445555, 5433284128909130351920391132⟩
def ThetaRun9.s3 : Seg := ⟨5433248796121979959812445555, 5433284128909130351920391132, 294553305, 1048576, [17978, 17980, 17982, 17984, 17986, 17989, 17991, 17993, 17995, 17997, 18000, 18002, 18004, 18006, 18008, 18011, 18013, 18015, 18017, 18019, 18022, 18024, 18026, 18028, 18030, 18033, 18035, 18037, 18039, 18041, 18044, 18046, 18048, 18050, 18052, 18055, 18057, 18059, 18061, 18063, 18066, 18068, 18070, 18072, 18074, 18077, 18079, 18081, 18083, 18085, 18088, 18090, 18092, 18094, 18096, 18099, 18101, 18103, 2238], 5471895335827016466950480802, 5471930910019546507380421984⟩
def ThetaRun9.s4 : Seg := ⟨5471895335827016466950480802, 5471930910019546507380421984, 296650457, 1048576, [18106, 18108, 18110, 18112, 18114, 18117, 18119, 18121, 18123, 18126, 18128, 18130, 18132, 18134, 18137, 18139, 18141, 18143, 18145, 18148, 18150, 18152, 18154, 18157, 18159, 18161, 18163, 18165, 18168, 18170, 18172, 18174, 18176, 18179, 18181, 18183, 18185, 18188, 18190, 18192, 18194, 18196, 18199, 18201, 18203, 18205, 18208, 18210, 18212, 18214, 18216, 18219, 18221, 18223, 18225, 18228, 18230, 13020], 5510545433932227411272458295, 5510581249080571494895151250⟩
def ThetaRun9.s5 : Seg := ⟨5510545433932227411272458295, 5510581249080571494895151250, 298747609, 1048576, [18234, 18236, 18238, 18240, 18243, 18245, 18247, 18249, 18251, 18254, 18256, 18258, 18260, 18263, 18265, 18267, 18269, 18271, 18274, 18276, 18278, 18280, 18283, 18285, 18287, 18289, 18292, 18294, 18296, 18298, 18300, 18303, 18305, 18307, 18309, 18312, 18314, 18316, 18318, 18321, 18323, 18325, 18327, 18330, 18332, 18334, 18336, 18339, 18341, 18343, 18345, 18347, 18350, 18352, 18354, 18356, 18359, 5700], 5549262732638740584632702605, 5549298789029045557136495056⟩
def ThetaRun9.s6 : Seg := ⟨5549262732638740584632702605, 5549298789029045557136495056, 300844761, 1048576, [18362, 18364, 18366, 18368, 18371, 18373, 18375, 18377, 18380, 18382, 18384, 18386, 18389, 18391, 18393, 18395, 18398, 18400, 18402, 18404, 18406, 18409, 18411, 18413, 18415, 18418, 18420, 18422, 18424, 18427, 18429, 18431, 18433, 18436, 18438, 18440, 18442, 18445, 18447, 18449, 18451, 18454, 18456, 18458, 18460, 18463, 18465, 18467, 18470, 18472, 18474, 18476, 18479, 18481, 18483, 18485, 16867], 5587932256880970798379829224, 5587968554659599999662247962⟩
def ThetaRun9.s7 : Seg := ⟨5587932256880970798379829224, 5587968554659599999662247962, 302941913, 1048576, [18490, 18492, 18494, 18496, 18499, 18501, 18503, 18505, 18508, 18510, 18512, 18514, 18517, 18519, 18521, 18523, 18526, 18528, 18530, 18533, 18535, 18537, 18539, 18542, 18544, 18546, 18548, 18551, 18553, 18555, 18557, 18560, 18562, 18564, 18567, 18569, 18571, 18573, 18576, 18578, 18580, 18582, 18585, 18587, 18589, 18591, 18594, 18596, 18598, 18601, 18603, 18605, 18607, 18610, 18612, 18614, 9674], 5626642172003059454873947321, 5626678710592460622884557827⟩
def ThetaRun9.s8 : Seg := ⟨5626642172003059454873947321, 5626678710592460622884557827, 305039065, 1048576, [18618, 18620, 18622, 18624, 18627, 18629, 18631, 18634, 18636, 18638, 18640, 18643, 18645, 18647, 18649, 18652, 18654, 18656, 18659, 18661, 18663, 18665, 18668, 18670, 18672, 18675, 18677, 18679, 18681, 18684, 18686, 18688, 18690, 18693, 18695, 18697, 18700, 18702, 18704, 18706, 18709, 18711, 18713, 18716, 18718, 18720, 18722, 18725, 18727, 18729, 18732, 18734, 18736, 18738, 18741, 18743, 2482], 5665325336587698664673145430, 5665362116327769555974088138⟩
def ThetaRun9.s9 : Seg := ⟨5665325336587698664673145430, 5665362116327769555974088138, 307136217, 1048576, [18746, 18748, 18750, 18752, 18755, 18757, 18759, 18762, 18764, 18766, 18769, 18771, 18773, 18775, 18778, 18780, 18782, 18785, 18787, 18789, 18791, 18794, 18796, 18798, 18801, 18803, 18805, 18807, 18810, 18812, 18814, 18817, 18819, 18821, 18824, 18826, 18828, 18830, 18833, 18835, 18837, 18840, 18842, 18844, 18847, 18849, 18851, 18853, 18856, 18858, 18860, 18863, 18865, 18867, 18870, 14162], 5704088356923444448556353056, 5704125377924744711240852371⟩
def ThetaRun9.s10 : Seg := ⟨5704088356923444448556353056, 5704125377924744711240852371, 309233369, 1048576, [18874, 18876, 18878, 18881, 18883, 18885, 18887, 18890, 18892, 18894, 18897, 18899, 18901, 18904, 18906, 18908, 18911, 18913, 18915, 18917, 18920, 18922, 18924, 18927, 18929, 18931, 18934, 18936, 18938, 18941, 18943, 18945, 18947, 18950, 18952, 18954, 18957, 18959, 18961, 18964, 18966, 18968, 18971, 18973, 18975, 18978, 18980, 18982, 18985, 18987, 18989, 18991, 18994, 18996, 18998, 7098], 5742733170666196459646322082, 5742770431876495509281007810⟩
def ThetaRun9.s11 : Seg := ⟨5742733170666196459646322082, 5742770431876495509281007810, 311330521, 1048576, [19002, 19004, 19006, 19009, 19011, 19013, 19016, 19018, 19020, 19022, 19025, 19027, 19029, 19032, 19034, 19036, 19039, 19041, 19043, 19046, 19048, 19050, 19053, 19055, 19057, 19060, 19062, 19064, 19067, 19069, 19071, 19074, 19076, 19078, 19081, 19083, 19085, 19088, 19090, 19092, 19095, 19097, 19099, 19102, 19104, 19106, 19109, 19111, 19113, 19116, 19118, 19120, 19123, 19125, 19127, 35], 5781460582769709592676943050, 5781498085647016956665605206⟩
def ThetaRun9.s12 : Seg := ⟨5781460582769709592676943050, 5781498085647016956665605206, 313427673, 1048576, [19130, 19132, 19134, 19137, 19139, 19141, 19144, 19146, 19148, 19151, 19153, 19155, 19158, 19160, 19162, 19165, 19167, 19169, 19172, 19174, 19176, 19179, 19181, 19183, 19186, 19188, 19190, 19193, 19195, 19197, 19200, 19202, 19204, 19207, 19209, 19212, 19214, 19216, 19219, 19221, 19223, 19226, 19228, 19230, 19233, 19235, 19237, 19240, 19242, 19244, 19247, 19249, 19251, 19254, 12228], 5820098373051050701732992923, 5820136115935667136407053951⟩
def ThetaRun9.s13 : Seg := ⟨5820098373051050701732992923, 5820136115935667136407053951, 315524825, 1048576, [19258, 19260, 19262, 19265, 19267, 19269, 19272, 19274, 19276, 19279, 19281, 19283, 19286, 19288, 19291, 19293, 19295, 19298, 19300, 19302, 19305, 19307, 19309, 19312, 19314, 19316, 19319, 19321, 19324, 19326, 19328, 19331, 19333, 19335, 19338, 19340, 19342, 19345, 19347, 19350, 19352, 19354, 19357, 19359, 19361, 19364, 19366, 19368, 19371, 19373, 19375, 19378, 19380, 19383, 5294], 5858795865400788110210926616, 5858833848720780255576661310⟩
def ThetaRun9.s14 : Seg := ⟨5858795865400788110210926616, 5858833848720780255576661310, 317621977, 1048576, [19386, 19388, 19390, 19393, 19395, 19397, 19400, 19402, 19405, 19407, 19409, 19412, 19414, 19416, 19419, 19421, 19424, 19426, 19428, 19431, 19433, 19435, 19438, 19440, 19442, 19445, 19447, 19450, 19452, 19454, 19457, 19459, 19461, 19464, 19466, 19469, 19471, 19473, 19476, 19478, 19480, 19483, 19485, 19488, 19490, 19492, 19495, 19497, 19500, 19502, 19504, 19507, 19509, 17871], 5897416119553388818031682008, 5897454343282781964676697291⟩
def ThetaRun9.s15 : Seg := ⟨5897416119553388818031682008, 5897454343282781964676697291, 319719129, 1048576, [19514, 19516, 19518, 19521, 19523, 19526, 19528, 19530, 19533, 19535, 19537, 19540, 19542, 19545, 19547, 19549, 19552, 19554, 19557, 19559, 19561, 19564, 19566, 19568, 19571, 19573, 19576, 19578, 19580, 19583, 19585, 19588, 19590, 19592, 19595, 19597, 19600, 19602, 19604, 19607, 19609, 19612, 19614, 19616, 19619, 19621, 19623, 19626, 19628, 19631, 19633, 19635, 19638, 11065], 5936056171497008951597465585, 5936094634945592668326664217⟩
def ThetaRun9.s16 : Seg := ⟨5936056171497008951597465585, 5936094634945592668326664217, 321816281, 1048576, [19642, 19644, 19646, 19649, 19651, 19654, 19656, 19658, 19661, 19663, 19666, 19668, 19670, 19673, 19675, 19678, 19680, 19682, 19685, 19687, 19690, 19692, 19694, 19697, 19699, 19702, 19704, 19706, 19709, 19711, 19714, 19716, 19718, 19721, 19723, 19726, 19728, 19731, 19733, 19735, 19738, 19740, 19743, 19745, 19747, 19750, 19752, 19755, 19757, 19759, 19762, 19764, 19767, 4260], 5974764021774186286816777572, 5974802725604360969356843745⟩

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