Theta certificate data, block 5

Definition
ThetaCertData_5
by @bwdaugherty · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)
analytic-number-theorynumber-theoryprime-numbers
Certificate records, block 5 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_5 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 ThetaRun5.s0 : Seg := ⟨2686621440056450102287486608, 2686639338065055257239939578, 145655513, 1048576, [8890, 8891, 8892, 8893, 8894, 8895, 8896, 8897, 8898, 8899, 8900, 8902, 8903, 8904, 8905, 8906, 8907, 8908, 8909, 8910, 8911, 8912, 8914, 8915, 8916, 8917, 8918, 8919, 8920, 8921, 8922, 8923, 8924, 8925, 8927, 8928, 8929, 8930, 8931, 8932, 8933, 8934, 8935, 8936, 8937, 8939, 8940, 8941, 8942, 8943, 8944, 8945, 8946, 8947, 8948, 8949, 8951, 8952, 8953, 8954, 8955, 8956, 8957, 8958, 8959, 8960, 8962, 8963, 8964, 8965, 8966, 8967, 8968, 8969, 8970, 8971, 8972, 8974, 8975, 8976, 8977, 8978, 8979, 8980, 8981, 8982, 8983, 8985, 8986, 8987, 8988, 8989, 8990, 8991, 8992, 8993, 8994, 8995, 8997, 8998, 8999, 9000, 9001, 9002, 9003, 9004, 9005, 9006, 9008, 9009, 9010, 9011, 9012, 9013, 9014, 9015, 9016, 1094], 2725360907250046309018687071, 2725379056475576663239684705⟩
def ThetaRun5.s1 : Seg := ⟨2725360907250046309018687071, 2725379056475576663239684705, 147752665, 1048576, [9018, 9019, 9020, 9021, 9022, 9023, 9024, 9025, 9026, 9028, 9029, 9030, 9031, 9032, 9033, 9034, 9035, 9036, 9037, 9039, 9040, 9041, 9042, 9043, 9044, 9045, 9046, 9047, 9048, 9050, 9051, 9052, 9053, 9054, 9055, 9056, 9057, 9058, 9060, 9061, 9062, 9063, 9064, 9065, 9066, 9067, 9068, 9069, 9071, 9072, 9073, 9074, 9075, 9076, 9077, 9078, 9079, 9081, 9082, 9083, 9084, 9085, 9086, 9087, 9088, 9089, 9091, 9092, 9093, 9094, 9095, 9096, 9097, 9098, 9099, 9101, 9102, 9103, 9104, 9105, 9106, 9107, 9108, 9109, 9111, 9112, 9113, 9114, 9115, 9116, 9117, 9118, 9119, 9121, 9122, 9123, 9124, 9125, 9126, 9127, 9128, 9129, 9131, 9132, 9133, 9134, 9135, 9136, 9137, 9138, 9140, 9141, 9142, 9143, 9144, 4301], 2764015071227490262891602790, 2764033470605960600208923694⟩
def ThetaRun5.s2 : Seg := ⟨2764015071227490262891602790, 2764033470605960600208923694, 149849817, 1048576, [9146, 9147, 9148, 9149, 9150, 9151, 9152, 9153, 9155, 9156, 9157, 9158, 9159, 9160, 9161, 9162, 9163, 9165, 9166, 9167, 9168, 9169, 9170, 9171, 9172, 9174, 9175, 9176, 9177, 9178, 9179, 9180, 9181, 9183, 9184, 9185, 9186, 9187, 9188, 9189, 9190, 9191, 9193, 9194, 9195, 9196, 9197, 9198, 9199, 9200, 9202, 9203, 9204, 9205, 9206, 9207, 9208, 9209, 9211, 9212, 9213, 9214, 9215, 9216, 9217, 9218, 9220, 9221, 9222, 9223, 9224, 9225, 9226, 9227, 9229, 9230, 9231, 9232, 9233, 9234, 9235, 9236, 9238, 9239, 9240, 9241, 9242, 9243, 9244, 9246, 9247, 9248, 9249, 9250, 9251, 9252, 9253, 9255, 9256, 9257, 9258, 9259, 9260, 9261, 9262, 9264, 9265, 9266, 9267, 9268, 9269, 9270, 9271, 8027], 2802635450858971589222047462, 2802654100296312655982325767⟩
def ThetaRun5.s3 : Seg := ⟨2802635450858971589222047462, 2802654100296312655982325767, 151946969, 1048576, [9274, 9275, 9276, 9277, 9278, 9279, 9280, 9282, 9283, 9284, 9285, 9286, 9287, 9288, 9289, 9291, 9292, 9293, 9294, 9295, 9296, 9297, 9299, 9300, 9301, 9302, 9303, 9304, 9305, 9306, 9308, 9309, 9310, 9311, 9312, 9313, 9314, 9316, 9317, 9318, 9319, 9320, 9321, 9322, 9324, 9325, 9326, 9327, 9328, 9329, 9330, 9332, 9333, 9334, 9335, 9336, 9337, 9338, 9339, 9341, 9342, 9343, 9344, 9345, 9346, 9347, 9349, 9350, 9351, 9352, 9353, 9354, 9355, 9357, 9358, 9359, 9360, 9361, 9362, 9363, 9365, 9366, 9367, 9368, 9369, 9370, 9371, 9373, 9374, 9375, 9376, 9377, 9378, 9379, 9381, 9382, 9383, 9384, 9385, 9386, 9387, 9389, 9390, 9391, 9392, 9393, 9394, 9396, 9397, 9398, 9399, 9400, 2865], 2841320305646635385367907302, 2841339205147929787961486663⟩
def ThetaRun5.s4 : Seg := ⟨2841320305646635385367907302, 2841339205147929787961486663, 154044121, 1048576, [9402, 9403, 9404, 9405, 9406, 9407, 9408, 9410, 9411, 9412, 9413, 9414, 9415, 9417, 9418, 9419, 9420, 9421, 9422, 9423, 9425, 9426, 9427, 9428, 9429, 9430, 9431, 9433, 9434, 9435, 9436, 9437, 9438, 9440, 9441, 9442, 9443, 9444, 9445, 9446, 9448, 9449, 9450, 9451, 9452, 9453, 9455, 9456, 9457, 9458, 9459, 9460, 9461, 9463, 9464, 9465, 9466, 9467, 9468, 9470, 9471, 9472, 9473, 9474, 9475, 9476, 9478, 9479, 9480, 9481, 9482, 9483, 9485, 9486, 9487, 9488, 9489, 9490, 9492, 9493, 9494, 9495, 9496, 9497, 9499, 9500, 9501, 9502, 9503, 9504, 9505, 9507, 9508, 9509, 9510, 9511, 9512, 9514, 9515, 9516, 9517, 9518, 9519, 9521, 9522, 9523, 9524, 9525, 9526, 9528, 7489], 2880037979555532151629340887, 2880057129249197877221987698⟩
def ThetaRun5.s5 : Seg := ⟨2880037979555532151629340887, 2880057129249197877221987698, 156141273, 1048576, [9530, 9531, 9532, 9533, 9534, 9535, 9537, 9538, 9539, 9540, 9541, 9542, 9544, 9545, 9546, 9547, 9548, 9549, 9551, 9552, 9553, 9554, 9555, 9556, 9558, 9559, 9560, 9561, 9562, 9563, 9565, 9566, 9567, 9568, 9569, 9570, 9572, 9573, 9574, 9575, 9576, 9577, 9579, 9580, 9581, 9582, 9583, 9584, 9586, 9587, 9588, 9589, 9590, 9591, 9593, 9594, 9595, 9596, 9597, 9598, 9600, 9601, 9602, 9603, 9604, 9606, 9607, 9608, 9609, 9610, 9611, 9613, 9614, 9615, 9616, 9617, 9618, 9620, 9621, 9622, 9623, 9624, 9625, 9627, 9628, 9629, 9630, 9631, 9633, 9634, 9635, 9636, 9637, 9638, 9640, 9641, 9642, 9643, 9644, 9645, 9647, 9648, 9649, 9650, 9651, 9653, 9654, 9655, 9656, 2971], 2918706972814093693218039359, 2918726372095859275927555278⟩
def ThetaRun5.s6 : Seg := ⟨2918706972814093693218039359, 2918726372095859275927555278, 158238425, 1048576, [9658, 9659, 9660, 9661, 9662, 9664, 9665, 9666, 9667, 9668, 9669, 9671, 9672, 9673, 9674, 9675, 9676, 9678, 9679, 9680, 9681, 9682, 9684, 9685, 9686, 9687, 9688, 9689, 9691, 9692, 9693, 9694, 9695, 9697, 9698, 9699, 9700, 9701, 9703, 9704, 9705, 9706, 9707, 9708, 9710, 9711, 9712, 9713, 9714, 9716, 9717, 9718, 9719, 9720, 9721, 9723, 9724, 9725, 9726, 9727, 9729, 9730, 9731, 9732, 9733, 9735, 9736, 9737, 9738, 9739, 9740, 9742, 9743, 9744, 9745, 9746, 9748, 9749, 9750, 9751, 9752, 9754, 9755, 9756, 9757, 9758, 9760, 9761, 9762, 9763, 9764, 9765, 9767, 9768, 9769, 9770, 9771, 9773, 9774, 9775, 9776, 9777, 9779, 9780, 9781, 9782, 9783, 8498], 2957367598551461390894554647, 2957387247421778270176385641⟩
def ThetaRun5.s7 : Seg := ⟨2957367598551461390894554647, 2957387247421778270176385641, 160335577, 1048576, [9786, 9787, 9788, 9789, 9790, 9792, 9793, 9794, 9795, 9796, 9798, 9799, 9800, 9801, 9802, 9804, 9805, 9806, 9807, 9808, 9810, 9811, 9812, 9813, 9814, 9816, 9817, 9818, 9819, 9820, 9822, 9823, 9824, 9825, 9826, 9828, 9829, 9830, 9831, 9832, 9834, 9835, 9836, 9837, 9838, 9840, 9841, 9842, 9843, 9844, 9846, 9847, 9848, 9849, 9850, 9852, 9853, 9854, 9855, 9856, 9858, 9859, 9860, 9861, 9862, 9864, 9865, 9866, 9867, 9868, 9870, 9871, 9872, 9873, 9874, 9876, 9877, 9878, 9879, 9880, 9882, 9883, 9884, 9885, 9886, 9888, 9889, 9890, 9891, 9892, 9894, 9895, 9896, 9897, 9899, 9900, 9901, 9902, 9903, 9905, 9906, 9907, 9908, 9909, 9911, 9912, 4621], 2996045563997079037358758137, 2996065462057467017191436996⟩
def ThetaRun5.s8 : Seg := ⟨2996045563997079037358758137, 2996065462057467017191436996, 162432729, 1048576, [9914, 9915, 9916, 9917, 9918, 9920, 9921, 9922, 9923, 9925, 9926, 9927, 9928, 9929, 9931, 9932, 9933, 9934, 9935, 9937, 9938, 9939, 9940, 9941, 9943, 9944, 9945, 9946, 9948, 9949, 9950, 9951, 9952, 9954, 9955, 9956, 9957, 9958, 9960, 9961, 9962, 9963, 9965, 9966, 9967, 9968, 9969, 9971, 9972, 9973, 9974, 9976, 9977, 9978, 9979, 9980, 9982, 9983, 9984, 9985, 9986, 9988, 9989, 9990, 9991, 9993, 9994, 9995, 9996, 9997, 9999, 10000, 10001, 10002, 10004, 10005, 10006, 10007, 10008, 10010, 10011, 10012, 10013, 10015, 10016, 10017, 10018, 10019, 10021, 10022, 10023, 10024, 10026, 10027, 10028, 10029, 10030, 10032, 10033, 10034, 10035, 10037, 10038, 10039, 10040, 1012], 3034758333961571027804147205, 3034778481642915483851875320⟩
def ThetaRun5.s9 : Seg := ⟨3034758333961571027804147205, 3034778481642915483851875320, 164529881, 1048576, [10042, 10043, 10044, 10045, 10047, 10048, 10049, 10050, 10051, 10053, 10054, 10055, 10056, 10058, 10059, 10060, 10061, 10062, 10064, 10065, 10066, 10067, 10069, 10070, 10071, 10072, 10074, 10075, 10076, 10077, 10078, 10080, 10081, 10082, 10083, 10085, 10086, 10087, 10088, 10090, 10091, 10092, 10093, 10094, 10096, 10097, 10098, 10099, 10101, 10102, 10103, 10104, 10106, 10107, 10108, 10109, 10110, 10112, 10113, 10114, 10115, 10117, 10118, 10119, 10120, 10122, 10123, 10124, 10125, 10127, 10128, 10129, 10130, 10131, 10133, 10134, 10135, 10136, 10138, 10139, 10140, 10141, 10143, 10144, 10145, 10146, 10148, 10149, 10150, 10151, 10153, 10154, 10155, 10156, 10157, 10159, 10160, 10161, 10162, 10164, 10165, 10166, 10167, 7825], 3073417613939104772701714897, 3073438010524226059056669663⟩
def ThetaRun5.s10 : Seg := ⟨3073417613939104772701714897, 3073438010524226059056669663, 166627033, 1048576, [10170, 10171, 10172, 10173, 10175, 10176, 10177, 10178, 10180, 10181, 10182, 10183, 10185, 10186, 10187, 10188, 10189, 10191, 10192, 10193, 10194, 10196, 10197, 10198, 10199, 10201, 10202, 10203, 10204, 10206, 10207, 10208, 10209, 10211, 10212, 10213, 10214, 10216, 10217, 10218, 10219, 10221, 10222, 10223, 10224, 10226, 10227, 10228, 10229, 10231, 10232, 10233, 10234, 10236, 10237, 10238, 10239, 10241, 10242, 10243, 10244, 10246, 10247, 10248, 10249, 10251, 10252, 10253, 10254, 10256, 10257, 10258, 10259, 10261, 10262, 10263, 10264, 10266, 10267, 10268, 10269, 10271, 10272, 10273, 10274, 10276, 10277, 10278, 10279, 10281, 10282, 10283, 10284, 10286, 10287, 10288, 10289, 10291, 10292, 10293, 10295, 10296, 4856], 3112127397472280147920492946, 3112148042950988836786303334⟩
def ThetaRun5.s11 : Seg := ⟨3112127397472280147920492946, 3112148042950988836786303334, 168724185, 1048576, [10298, 10299, 10300, 10301, 10303, 10304, 10305, 10306, 10308, 10309, 10310, 10311, 10313, 10314, 10315, 10316, 10318, 10319, 10320, 10322, 10323, 10324, 10325, 10327, 10328, 10329, 10330, 10332, 10333, 10334, 10335, 10337, 10338, 10339, 10340, 10342, 10343, 10344, 10345, 10347, 10348, 10349, 10351, 10352, 10353, 10354, 10356, 10357, 10358, 10359, 10361, 10362, 10363, 10364, 10366, 10367, 10368, 10370, 10371, 10372, 10373, 10375, 10376, 10377, 10378, 10380, 10381, 10382, 10383, 10385, 10386, 10387, 10389, 10390, 10391, 10392, 10394, 10395, 10396, 10397, 10399, 10400, 10401, 10402, 10404, 10405, 10406, 10408, 10409, 10410, 10411, 10413, 10414, 10415, 10416, 10418, 10419, 10420, 10422, 10423, 10424, 2143], 3150823770753056470878086712, 3150844665077886432030878506⟩
def ThetaRun5.s12 : Seg := ⟨3150823770753056470878086712, 3150844665077886432030878506, 170821337, 1048576, [10426, 10427, 10428, 10429, 10431, 10432, 10433, 10435, 10436, 10437, 10438, 10440, 10441, 10442, 10443, 10445, 10446, 10447, 10449, 10450, 10451, 10452, 10454, 10455, 10456, 10457, 10459, 10460, 10461, 10463, 10464, 10465, 10466, 10468, 10469, 10470, 10472, 10473, 10474, 10475, 10477, 10478, 10479, 10480, 10482, 10483, 10484, 10486, 10487, 10488, 10489, 10491, 10492, 10493, 10495, 10496, 10497, 10498, 10500, 10501, 10502, 10504, 10505, 10506, 10507, 10509, 10510, 10511, 10513, 10514, 10515, 10516, 10518, 10519, 10520, 10521, 10523, 10524, 10525, 10527, 10528, 10529, 10530, 10532, 10533, 10534, 10536, 10537, 10538, 10539, 10541, 10542, 10543, 10545, 10546, 10547, 10548, 10550, 10551, 10243], 3189555703573659562035668102, 3189576847140863766097230471⟩
def ThetaRun5.s13 : Seg := ⟨3189555703573659562035668102, 3189576847140863766097230471, 172918489, 1048576, [10554, 10555, 10556, 10557, 10559, 10560, 10561, 10563, 10564, 10565, 10566, 10568, 10569, 10570, 10572, 10573, 10574, 10576, 10577, 10578, 10579, 10581, 10582, 10583, 10585, 10586, 10587, 10588, 10590, 10591, 10592, 10594, 10595, 10596, 10597, 10599, 10600, 10601, 10603, 10604, 10605, 10607, 10608, 10609, 10610, 10612, 10613, 10614, 10616, 10617, 10618, 10620, 10621, 10622, 10623, 10625, 10626, 10627, 10629, 10630, 10631, 10632, 10634, 10635, 10636, 10638, 10639, 10640, 10642, 10643, 10644, 10645, 10647, 10648, 10649, 10651, 10652, 10653, 10655, 10656, 10657, 10658, 10660, 10661, 10662, 10664, 10665, 10666, 10668, 10669, 10670, 10671, 10673, 10674, 10675, 10677, 10678, 10679, 8177], 3228228761966195763352775425, 3228250153852001755916859278⟩
def ThetaRun5.s14 : Seg := ⟨3228228761966195763352775425, 3228250153852001755916859278, 175015641, 1048576, [10682, 10683, 10684, 10686, 10687, 10688, 10689, 10691, 10692, 10693, 10695, 10696, 10697, 10699, 10700, 10701, 10702, 10704, 10705, 10706, 10708, 10709, 10710, 10712, 10713, 10714, 10716, 10717, 10718, 10719, 10721, 10722, 10723, 10725, 10726, 10727, 10729, 10730, 10731, 10733, 10734, 10735, 10737, 10738, 10739, 10740, 10742, 10743, 10744, 10746, 10747, 10748, 10750, 10751, 10752, 10754, 10755, 10756, 10757, 10759, 10760, 10761, 10763, 10764, 10765, 10767, 10768, 10769, 10771, 10772, 10773, 10775, 10776, 10777, 10779, 10780, 10781, 10782, 10784, 10785, 10786, 10788, 10789, 10790, 10792, 10793, 10794, 10796, 10797, 10798, 10800, 10801, 10802, 10804, 10805, 10806, 10808, 6365], 3266985096306979525918108669, 3267006736720052710868714903⟩
def ThetaRun5.s15 : Seg := ⟨3266985096306979525918108669, 3267006736720052710868714903, 177112793, 1048576, [10810, 10811, 10812, 10814, 10815, 10816, 10818, 10819, 10820, 10821, 10823, 10824, 10825, 10827, 10828, 10829, 10831, 10832, 10833, 10835, 10836, 10837, 10839, 10840, 10841, 10843, 10844, 10845, 10847, 10848, 10849, 10851, 10852, 10853, 10855, 10856, 10857, 10859, 10860, 10861, 10863, 10864, 10865, 10866, 10868, 10869, 10870, 10872, 10873, 10874, 10876, 10877, 10878, 10880, 10881, 10882, 10884, 10885, 10886, 10888, 10889, 10890, 10892, 10893, 10894, 10896, 10897, 10898, 10900, 10901, 10902, 10904, 10905, 10906, 10908, 10909, 10910, 10912, 10913, 10914, 10916, 10917, 10918, 10920, 10921, 10922, 10924, 10925, 10926, 10928, 10929, 10930, 10932, 10933, 10934, 10936, 4815], 3305681493358510415816989595, 3305703381720983134465291019⟩
def ThetaRun5.s16 : Seg := ⟨3305681493358510415816989595, 3305703381720983134465291019, 179209945, 1048576, [10938, 10939, 10940, 10942, 10943, 10944, 10946, 10947, 10948, 10950, 10951, 10952, 10954, 10955, 10956, 10958, 10959, 10960, 10962, 10963, 10964, 10966, 10967, 10968, 10970, 10971, 10972, 10974, 10975, 10976, 10978, 10979, 10980, 10982, 10983, 10984, 10986, 10987, 10988, 10990, 10991, 10992, 10994, 10995, 10997, 10998, 10999, 11001, 11002, 11003, 11005, 11006, 11007, 11009, 11010, 11011, 11013, 11014, 11015, 11017, 11018, 11019, 11021, 11022, 11023, 11025, 11026, 11027, 11029, 11030, 11031, 11033, 11034, 11036, 11037, 11038, 11040, 11041, 11042, 11044, 11045, 11046, 11048, 11049, 11050, 11052, 11053, 11054, 11056, 11057, 11058, 11060, 11061, 11062, 11064, 3519], 3344336131464228100347825928, 3344358267474907607021862388⟩

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