Theta certificate data, block 8

Definition

ThetaCertData_8

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

analytic-number-theorynumber-theoryprime-numbers

Certificate records, block 8 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_8 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 ThetaRun8.s0 : Seg := ⟨4659568040436641427963731241, 4659598524762391814059022623, 252610265, 1048576, [15418, 15419, 15421, 15423, 15425, 15427, 15429, 15431, 15433, 15435, 15436, 15438, 15440, 15442, 15444, 15446, 15448, 15450, 15452, 15453, 15455, 15457, 15459, 15461, 15463, 15465, 15467, 15469, 15470, 15472, 15474, 15476, 15478, 15480, 15482, 15484, 15486, 15487, 15489, 15491, 15493, 15495, 15497, 15499, 15501, 15503, 15504, 15506, 15508, 15510, 15512, 15514, 15516, 15518, 15520, 15521, 15523, 15525, 15527, 15529, 15531, 15533, 15535, 15537, 15539, 15540, 15542, 11423], 4698266920170430861215405400, 4698297647893003864084269178⟩
def ThetaRun8.s1 : Seg := ⟨4698266920170430861215405400, 4698297647893003864084269178, 254707417, 1048576, [15546, 15548, 15549, 15551, 15553, 15555, 15557, 15559, 15561, 15563, 15565, 15566, 15568, 15570, 15572, 15574, 15576, 15578, 15580, 15582, 15584, 15586, 15587, 15589, 15591, 15593, 15595, 15597, 15599, 15601, 15603, 15605, 15606, 15608, 15610, 15612, 15614, 15616, 15618, 15620, 15622, 15624, 15626, 15627, 15629, 15631, 15633, 15635, 15637, 15639, 15641, 15643, 15645, 15647, 15648, 15650, 15652, 15654, 15656, 15658, 15660, 15662, 15664, 15666, 15668, 15669, 15671, 2812], 4736892965220677784811504743, 4736923935882115568972889273⟩
def ThetaRun8.s2 : Seg := ⟨4736892965220677784811504743, 4736923935882115568972889273, 256804569, 1048576, [15674, 15676, 15677, 15679, 15681, 15683, 15685, 15687, 15689, 15691, 15693, 15695, 15697, 15698, 15700, 15702, 15704, 15706, 15708, 15710, 15712, 15714, 15716, 15718, 15720, 15722, 15723, 15725, 15727, 15729, 15731, 15733, 15735, 15737, 15739, 15741, 15743, 15745, 15746, 15748, 15750, 15752, 15754, 15756, 15758, 15760, 15762, 15764, 15766, 15768, 15770, 15771, 15773, 15775, 15777, 15779, 15781, 15783, 15785, 15787, 15789, 15791, 15793, 15795, 15797, 15798, 10003], 4775642493526451533895421787, 4775673707505171178379507432⟩
def ThetaRun8.s3 : Seg := ⟨4775642493526451533895421787, 4775673707505171178379507432, 258901721, 1048576, [15802, 15804, 15805, 15807, 15809, 15811, 15813, 15815, 15817, 15819, 15821, 15823, 15825, 15827, 15829, 15831, 15832, 15834, 15836, 15838, 15840, 15842, 15844, 15846, 15848, 15850, 15852, 15854, 15856, 15858, 15860, 15862, 15863, 15865, 15867, 15869, 15871, 15873, 15875, 15877, 15879, 15881, 15883, 15885, 15887, 15889, 15891, 15893, 15894, 15896, 15898, 15900, 15902, 15904, 15906, 15908, 15910, 15912, 15914, 15916, 15918, 15920, 15922, 15924, 15926, 15927, 1521], 4814311378564062542691988013, 4814342835820386372358846521⟩
def ThetaRun8.s4 : Seg := ⟨4814311378564062542691988013, 4814342835820386372358846521, 260998873, 1048576, [15930, 15932, 15933, 15935, 15937, 15939, 15941, 15943, 15945, 15947, 15949, 15951, 15953, 15955, 15957, 15959, 15961, 15963, 15965, 15967, 15969, 15970, 15972, 15974, 15976, 15978, 15980, 15982, 15984, 15986, 15988, 15990, 15992, 15994, 15996, 15998, 16000, 16002, 16004, 16006, 16008, 16010, 16011, 16013, 16015, 16017, 16019, 16021, 16023, 16025, 16027, 16029, 16031, 16033, 16035, 16037, 16039, 16041, 16043, 16045, 16047, 16049, 16051, 16053, 16055, 9096], 4853068163710553336377826359, 4853099864073916281687519197⟩
def ThetaRun8.s5 : Seg := ⟨4853068163710553336377826359, 4853099864073916281687519197, 263096025, 1048576, [16058, 16060, 16062, 16063, 16065, 16067, 16069, 16071, 16073, 16075, 16077, 16079, 16081, 16083, 16085, 16087, 16089, 16091, 16093, 16095, 16097, 16099, 16101, 16103, 16105, 16107, 16109, 16111, 16113, 16115, 16117, 16118, 16120, 16122, 16124, 16126, 16128, 16130, 16132, 16134, 16136, 16138, 16140, 16142, 16144, 16146, 16148, 16150, 16152, 16154, 16156, 16158, 16160, 16162, 16164, 16166, 16168, 16170, 16172, 16174, 16176, 16178, 16180, 16182, 16184, 742], 4891659892496003602161689025, 4891691835600807794506933182⟩
def ThetaRun8.s6 : Seg := ⟨4891659892496003602161689025, 4891691835600807794506933182, 265193177, 1048576, [16186, 16188, 16190, 16192, 16194, 16195, 16197, 16199, 16201, 16203, 16205, 16207, 16209, 16211, 16213, 16215, 16217, 16219, 16221, 16223, 16225, 16227, 16229, 16231, 16233, 16235, 16237, 16239, 16241, 16243, 16245, 16247, 16249, 16251, 16253, 16255, 16257, 16259, 16261, 16263, 16265, 16267, 16269, 16271, 16273, 16275, 16277, 16279, 16281, 16283, 16285, 16287, 16289, 16291, 16293, 16295, 16297, 16299, 16301, 16303, 16305, 16307, 16309, 16311, 8699], 4930342123312467713015759346, 4930374308840279460525401779⟩
def ThetaRun8.s7 : Seg := ⟨4930342123312467713015759346, 4930374308840279460525401779, 267290329, 1048576, [16314, 16316, 16318, 16320, 16322, 16324, 16326, 16328, 16330, 16332, 16334, 16336, 16338, 16340, 16342, 16344, 16345, 16347, 16349, 16351, 16353, 16355, 16357, 16359, 16361, 16363, 16365, 16367, 16369, 16371, 16373, 16375, 16377, 16379, 16381, 16383, 16385, 16387, 16389, 16391, 16393, 16395, 16397, 16399, 16401, 16403, 16405, 16407, 16409, 16411, 16413, 16415, 16417, 16419, 16421, 16423, 16425, 16428, 16430, 16432, 16434, 16436, 16438, 16440, 489], 4969082627486063789252375509, 4969115056543276803609735674⟩
def ThetaRun8.s8 : Seg := ⟨4969082627486063789252375509, 4969115056543276803609735674, 269387481, 1048576, [16442, 16444, 16446, 16448, 16450, 16452, 16454, 16456, 16458, 16460, 16462, 16464, 16466, 16468, 16470, 16472, 16474, 16476, 16478, 16480, 16482, 16484, 16486, 16488, 16490, 16492, 16494, 16496, 16498, 16500, 16502, 16504, 16506, 16508, 16510, 16512, 16514, 16516, 16518, 16520, 16522, 16524, 16526, 16528, 16530, 16532, 16534, 16536, 16538, 16540, 16542, 16544, 16546, 16548, 16550, 16552, 16554, 16556, 16558, 16560, 16562, 16564, 16567, 8823], 5007605509692626548658589843, 5007638179997158828959893201⟩
def ThetaRun8.s9 : Seg := ⟨5007605509692626548658589843, 5007638179997158828959893201, 271484633, 1048576, [16570, 16572, 16574, 16576, 16578, 16580, 16582, 16584, 16586, 16588, 16590, 16592, 16594, 16596, 16598, 16600, 16602, 16604, 16606, 16608, 16610, 16612, 16614, 16616, 16618, 16620, 16622, 16624, 16626, 16628, 16630, 16632, 16634, 16636, 16639, 16641, 16643, 16645, 16647, 16649, 16651, 16653, 16655, 16657, 16659, 16661, 16663, 16665, 16667, 16669, 16671, 16673, 16675, 16677, 16679, 16681, 16683, 16685, 16687, 16689, 16691, 16693, 16695, 731], 5046293833254842060174868287, 5046326746520606494299279088⟩
def ThetaRun8.s10 : Seg := ⟨5046293833254842060174868287, 5046326746520606494299279088, 273581785, 1048576, [16698, 16700, 16702, 16704, 16706, 16708, 16710, 16712, 16714, 16716, 16718, 16720, 16722, 16724, 16726, 16728, 16730, 16732, 16734, 16736, 16738, 16740, 16743, 16745, 16747, 16749, 16751, 16753, 16755, 16757, 16759, 16761, 16763, 16765, 16767, 16769, 16771, 16773, 16775, 16777, 16779, 16781, 16783, 16785, 16788, 16790, 16792, 16794, 16796, 16798, 16800, 16802, 16804, 16806, 16808, 16810, 16812, 16814, 16816, 16818, 16820, 16822, 9460], 5085078791921477696688267578, 5085111947844833572918070121⟩
def ThetaRun8.s11 : Seg := ⟨5085078791921477696688267578, 5085111947844833572918070121, 275678937, 1048576, [16826, 16828, 16830, 16832, 16834, 16836, 16838, 16840, 16842, 16844, 16846, 16848, 16850, 16852, 16854, 16856, 16858, 16861, 16863, 16865, 16867, 16869, 16871, 16873, 16875, 16877, 16879, 16881, 16883, 16885, 16887, 16889, 16891, 16894, 16896, 16898, 16900, 16902, 16904, 16906, 16908, 16910, 16912, 16914, 16916, 16918, 16920, 16922, 16924, 16927, 16929, 16931, 16933, 16935, 16937, 16939, 16941, 16943, 16945, 16947, 16949, 16951, 1495], 5123809028095500153675821810, 5123842426871033966881381867⟩
def ThetaRun8.s12 : Seg := ⟨5123809028095500153675821810, 5123842426871033966881381867, 277776089, 1048576, [16954, 16956, 16958, 16960, 16962, 16964, 16966, 16968, 16970, 16972, 16974, 16976, 16978, 16981, 16983, 16985, 16987, 16989, 16991, 16993, 16995, 16997, 16999, 17001, 17003, 17005, 17007, 17010, 17012, 17014, 17016, 17018, 17020, 17022, 17024, 17026, 17028, 17030, 17032, 17035, 17037, 17039, 17041, 17043, 17045, 17047, 17049, 17051, 17053, 17055, 17057, 17059, 17062, 17064, 17066, 17068, 17070, 17072, 17074, 17076, 17078, 10609], 5162439875261410389037996913, 5162473515633095275912475236⟩
def ThetaRun8.s13 : Seg := ⟨5162439875261410389037996913, 5162473515633095275912475236, 279873241, 1048576, [17082, 17084, 17086, 17088, 17090, 17092, 17094, 17096, 17098, 17100, 17102, 17105, 17107, 17109, 17111, 17113, 17115, 17117, 17119, 17121, 17123, 17125, 17128, 17130, 17132, 17134, 17136, 17138, 17140, 17142, 17144, 17146, 17148, 17151, 17153, 17155, 17157, 17159, 17161, 17163, 17165, 17167, 17169, 17171, 17174, 17176, 17178, 17180, 17182, 17184, 17186, 17188, 17190, 17192, 17195, 17197, 17199, 17201, 17203, 17205, 17207, 2773], 5201169567905987548280302679, 5201203450767847023271030896⟩
def ThetaRun8.s14 : Seg := ⟨5201169567905987548280302679, 5201203450767847023271030896, 281970393, 1048576, [17210, 17212, 17214, 17216, 17218, 17220, 17222, 17224, 17226, 17229, 17231, 17233, 17235, 17237, 17239, 17241, 17243, 17245, 17247, 17250, 17252, 17254, 17256, 17258, 17260, 17262, 17264, 17266, 17269, 17271, 17273, 17275, 17277, 17279, 17281, 17283, 17285, 17288, 17290, 17292, 17294, 17296, 17298, 17300, 17302, 17304, 17307, 17309, 17311, 17313, 17315, 17317, 17319, 17321, 17323, 17326, 17328, 17330, 17332, 17334, 12270], 5239822172268689868955868359, 5239856296738148607078309462⟩
def ThetaRun8.s15 : Seg := ⟨5239822172268689868955868359, 5239856296738148607078309462, 284067545, 1048576, [17338, 17340, 17342, 17344, 17346, 17348, 17350, 17352, 17355, 17357, 17359, 17361, 17363, 17365, 17367, 17369, 17372, 17374, 17376, 17378, 17380, 17382, 17384, 17386, 17388, 17391, 17393, 17395, 17397, 17399, 17401, 17403, 17405, 17408, 17410, 17412, 17414, 17416, 17418, 17420, 17422, 17425, 17427, 17429, 17431, 17433, 17435, 17437, 17439, 17442, 17444, 17446, 17448, 17450, 17452, 17454, 17457, 17459, 17461, 17463, 4564], 5278421206900378207248870252, 5278455572624953872158810886⟩
def ThetaRun8.s16 : Seg := ⟨5278421206900378207248870252, 5278455572624953872158810886, 286164697, 1048576, [17466, 17468, 17470, 17472, 17474, 17476, 17478, 17481, 17483, 17485, 17487, 17489, 17491, 17493, 17495, 17498, 17500, 17502, 17504, 17506, 17508, 17510, 17513, 17515, 17517, 17519, 17521, 17523, 17525, 17528, 17530, 17532, 17534, 17536, 17538, 17540, 17543, 17545, 17547, 17549, 17551, 17553, 17555, 17558, 17560, 17562, 17564, 17566, 17568, 17570, 17573, 17575, 17577, 17579, 17581, 17583, 17585, 17588, 17590, 14447], 5317086857365690478441380286, 5317121464834516731932589873⟩

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