Theta certificate data, block 13

Definition

ThetaCertData_13

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

analytic-number-theorynumber-theoryprime-numbers

Certificate records, block 13 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_13 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 ThetaRun13.s0 : Seg := ⟨7947694300911199595929133541, 7947745156654584578230695874, 430868185, 1048576, [26298, 26301, 26304, 26307, 26310, 26314, 26317, 26320, 26323, 26327, 26330, 26333, 26336, 26339, 26343, 26346, 26349, 26352, 26355, 26359, 26362, 26365, 26368, 26372, 26375, 26378, 26381, 26384, 26388, 26391, 26394, 26397, 26401, 26404, 26407, 26410, 26413, 26417, 26420, 20586], 7986359013280434675778102189, 7986410105337758963415924408⟩
def ThetaRun13.s1 : Seg := ⟨7986359013280434675778102189, 7986410105337758963415924408, 432965337, 1048576, [26426, 26429, 26432, 26435, 26439, 26442, 26445, 26448, 26451, 26455, 26458, 26461, 26464, 26468, 26471, 26474, 26477, 26480, 26484, 26487, 26490, 26493, 26497, 26500, 26503, 26506, 26510, 26513, 26516, 26519, 26523, 26526, 26529, 26532, 26536, 26539, 26542, 26545, 26548, 15583], 8025062870878928280549155119, 8025114199030219405100236380⟩
def ThetaRun13.s2 : Seg := ⟨8025062870878928280549155119, 8025114199030219405100236380, 435062489, 1048576, [26554, 26557, 26560, 26563, 26567, 26570, 26573, 26576, 26580, 26583, 26586, 26589, 26593, 26596, 26599, 26602, 26606, 26609, 26612, 26615, 26619, 26622, 26625, 26628, 26632, 26635, 26638, 26641, 26645, 26648, 26651, 26654, 26658, 26661, 26664, 26667, 26671, 26674, 26677, 10576], 8063701977081066645457745855, 8063753540876533824507555282⟩
def ThetaRun13.s3 : Seg := ⟨8063701977081066645457745855, 8063753540876533824507555282, 437159641, 1048576, [26682, 26685, 26688, 26691, 26695, 26698, 26701, 26704, 26708, 26711, 26714, 26717, 26721, 26724, 26727, 26731, 26734, 26737, 26740, 26744, 26747, 26750, 26753, 26757, 26760, 26763, 26766, 26770, 26773, 26776, 26779, 26783, 26786, 26789, 26793, 26796, 26799, 26802, 26806, 5576], 8102405823817072381060880058, 8102457624026660964778516215⟩
def ThetaRun13.s4 : Seg := ⟨8102405823817072381060880058, 8102457624026660964778516215, 439256793, 1048576, [26810, 26813, 26816, 26819, 26823, 26826, 26829, 26833, 26836, 26839, 26842, 26846, 26849, 26852, 26855, 26859, 26862, 26865, 26869, 26872, 26875, 26878, 26882, 26885, 26888, 26892, 26895, 26898, 26901, 26905, 26908, 26911, 26915, 26918, 26921, 26924, 26928, 26931, 26934, 572], 8141116757724204043075297491, 8141168795208065916930767330⟩
def ThetaRun13.s5 : Seg := ⟨8141116757724204043075297491, 8141168795208065916930767330, 441353945, 1048576, [26938, 26941, 26944, 26947, 26951, 26954, 26957, 26961, 26964, 26967, 26971, 26974, 26977, 26980, 26984, 26987, 26990, 26994, 26997, 27000, 27003, 27007, 27010, 27013, 27017, 27020, 27023, 27027, 27030, 27033, 27036, 27040, 27043, 27046, 27050, 27053, 27056, 27060, 22631], 8179899361912777042614433820, 8179951636344246840122847498⟩
def ThetaRun13.s6 : Seg := ⟨8179899361912777042614433820, 8179951636344246840122847498, 443451097, 1048576, [27066, 27069, 27072, 27076, 27079, 27082, 27085, 27089, 27092, 27095, 27099, 27102, 27105, 27109, 27112, 27115, 27119, 27122, 27125, 27128, 27132, 27135, 27138, 27142, 27145, 27148, 27152, 27155, 27158, 27162, 27165, 27168, 27172, 27175, 27178, 27181, 27185, 27188, 17756], 8218497966763436515179996843, 8218550476398303379004324690⟩
def ThetaRun13.s7 : Seg := ⟨8218497966763436515179996843, 8218550476398303379004324690, 445548249, 1048576, [27194, 27197, 27200, 27204, 27207, 27210, 27214, 27217, 27220, 27223, 27227, 27230, 27233, 27237, 27240, 27243, 27247, 27250, 27253, 27257, 27260, 27263, 27267, 27270, 27273, 27277, 27280, 27283, 27287, 27290, 27293, 27297, 27300, 27303, 27307, 27310, 27313, 27317, 12883], 8257221430065355764962385952, 8257274175503012839908451923⟩
def ThetaRun13.s8 : Seg := ⟨8257221430065355764962385952, 8257274175503012839908451923, 447645401, 1048576, [27322, 27325, 27328, 27332, 27335, 27338, 27342, 27345, 27348, 27352, 27355, 27358, 27362, 27365, 27368, 27372, 27375, 27378, 27382, 27385, 27388, 27392, 27395, 27398, 27402, 27405, 27408, 27412, 27415, 27418, 27422, 27425, 27429, 27432, 27435, 27439, 27442, 27445, 8007], 8295944815914920924117272507, 8295997797281942757250916524⟩
def ThetaRun13.s9 : Seg := ⟨8295944815914920924117272507, 8295997797281942757250916524, 449742553, 1048576, [27450, 27453, 27456, 27460, 27463, 27466, 27470, 27473, 27476, 27480, 27483, 27486, 27490, 27493, 27497, 27500, 27503, 27507, 27510, 27513, 27517, 27520, 27523, 27527, 27530, 27533, 27537, 27540, 27544, 27547, 27550, 27554, 27557, 27560, 27564, 27567, 27570, 27574, 3133], 8334600080080833523108500569, 8334653297651831740756624499⟩
def ThetaRun13.s10 : Seg := ⟨8334600080080833523108500569, 8334653297651831740756624499, 451839705, 1048576, [27578, 27581, 27584, 27588, 27591, 27594, 27598, 27601, 27605, 27608, 27611, 27615, 27618, 27621, 27625, 27628, 27632, 27635, 27638, 27642, 27645, 27648, 27652, 27655, 27659, 27662, 27665, 27669, 27672, 27675, 27679, 27682, 27686, 27689, 27692, 27696, 27699, 25958], 8373265814369477881061274900, 8373319268364776975545540666⟩
def ThetaRun13.s11 : Seg := ⟨8373265814369477881061274900, 8373319268364776975545540666, 453936857, 1048576, [27706, 27709, 27712, 27716, 27719, 27723, 27726, 27729, 27733, 27736, 27739, 27743, 27746, 27750, 27753, 27756, 27760, 27763, 27767, 27770, 27773, 27777, 27780, 27783, 27787, 27790, 27794, 27797, 27800, 27804, 27807, 27811, 27814, 27817, 27821, 27824, 27828, 21213], 8411987216062711144334188757, 8412040906005646934325863710⟩
def ThetaRun13.s12 : Seg := ⟨8411987216062711144334188757, 8412040906005646934325863710, 456034009, 1048576, [27834, 27837, 27840, 27844, 27847, 27851, 27854, 27857, 27861, 27864, 27868, 27871, 27874, 27878, 27881, 27885, 27888, 27891, 27895, 27898, 27902, 27905, 27908, 27912, 27915, 27919, 27922, 27925, 27929, 27932, 27936, 27939, 27943, 27946, 27949, 27953, 27956, 16467], 8450641765353823906320005878, 8450695690358043947017179089⟩
def ThetaRun13.s13 : Seg := ⟨8450641765353823906320005878, 8450695690358043947017179089, 458131161, 1048576, [27962, 27965, 27968, 27972, 27975, 27979, 27982, 27986, 27989, 27992, 27996, 27999, 28003, 28006, 28009, 28013, 28016, 28020, 28023, 28027, 28030, 28033, 28037, 28040, 28044, 28047, 28050, 28054, 28057, 28061, 28064, 28068, 28071, 28074, 28078, 28081, 28085, 11720], 8489276493694999877269588324, 8489330653619120861328062940⟩
def ThetaRun13.s14 : Seg := ⟨8489276493694999877269588324, 8489330653619120861328062940, 460228313, 1048576, [28090, 28093, 28096, 28100, 28103, 28107, 28110, 28114, 28117, 28120, 28124, 28127, 28131, 28134, 28138, 28141, 28145, 28148, 28151, 28155, 28158, 28162, 28165, 28169, 28172, 28175, 28179, 28182, 28186, 28189, 28193, 28196, 28200, 28203, 28206, 28210, 28213, 6974], 8527962738542460799927945379, 8528017134022432103334034698⟩
def ThetaRun13.s15 : Seg := ⟨8527962738542460799927945379, 8528017134022432103334034698, 462325465, 1048576, [28218, 28221, 28224, 28228, 28231, 28235, 28238, 28242, 28245, 28249, 28252, 28256, 28259, 28262, 28266, 28269, 28273, 28276, 28280, 28283, 28287, 28290, 28293, 28297, 28300, 28304, 28307, 28311, 28314, 28318, 28321, 28325, 28328, 28331, 28335, 28338, 28342, 2228], 8566725872915104404343026707, 8566780505025730920312829111⟩
def ThetaRun13.s16 : Seg := ⟨8566725872915104404343026707, 8566780505025730920312829111, 464422617, 1048576, [28346, 28349, 28353, 28356, 28359, 28363, 28366, 28370, 28373, 28377, 28380, 28384, 28387, 28391, 28394, 28398, 28401, 28404, 28408, 28411, 28415, 28418, 28422, 28425, 28429, 28432, 28436, 28439, 28443, 28446, 28450, 28453, 28457, 28460, 28463, 28467, 25951], 8605430414026677136676710468, 8605485282318700842916716419⟩

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