Theta certificate data, block 14

Definition

ThetaCertData_14

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

analytic-number-theorynumber-theoryprime-numbers

Certificate records, block 14 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_14 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 ThetaRun14.s0 : Seg := ⟨8605430414026677136676710468, 8605485282318700842916716419, 466519769, 1048576, [28474, 28477, 28481, 28484, 28488, 28491, 28494, 28498, 28501, 28505, 28508, 28512, 28515, 28519, 28522, 28526, 28529, 28533, 28536, 28540, 28543, 28547, 28550, 28554, 28557, 28561, 28564, 28568, 28571, 28575, 28578, 28582, 28585, 28589, 28592, 28596, 21331], 8644143302263778390598640684, 8644198406023950203439608828⟩
def ThetaRun14.s1 : Seg := ⟨8644143302263778390598640684, 8644198406023950203439608828, 468616921, 1048576, [28602, 28605, 28609, 28612, 28616, 28619, 28623, 28626, 28630, 28633, 28637, 28640, 28644, 28647, 28651, 28654, 28658, 28661, 28665, 28668, 28672, 28675, 28679, 28682, 28686, 28689, 28693, 28696, 28700, 28703, 28707, 28710, 28714, 28717, 28721, 28724, 16708], 8682816988719784636410494487, 8682872327256740222025982938⟩
def ThetaRun14.s2 : Seg := ⟨8682816988719784636410494487, 8682872327256740222025982938, 470714073, 1048576, [28730, 28733, 28737, 28740, 28744, 28747, 28751, 28754, 28758, 28761, 28765, 28768, 28772, 28775, 28779, 28782, 28786, 28789, 28793, 28796, 28800, 28803, 28807, 28810, 28814, 28817, 28821, 28824, 28828, 28831, 28835, 28839, 28842, 28846, 28849, 28853, 12097], 8721458034719835402692922819, 8721513607835222906753953886⟩
def ThetaRun14.s3 : Seg := ⟨8721458034719835402692922819, 8721513607835222906753953886, 472811225, 1048576, [28858, 28861, 28865, 28868, 28872, 28875, 28879, 28882, 28886, 28889, 28893, 28896, 28900, 28903, 28907, 28910, 28914, 28918, 28921, 28925, 28928, 28932, 28935, 28939, 28942, 28946, 28949, 28953, 28956, 28960, 28963, 28967, 28971, 28974, 28978, 28981, 7480], 8760059020180432351259665120, 8760114827893244529499711669⟩
def ThetaRun14.s4 : Seg := ⟨8760059020180432351259665120, 8760114827893244529499711669, 474908377, 1048576, [28986, 28989, 28993, 28996, 29000, 29003, 29007, 29010, 29014, 29017, 29021, 29025, 29028, 29032, 29035, 29039, 29042, 29046, 29049, 29053, 29056, 29060, 29064, 29067, 29071, 29074, 29078, 29081, 29085, 29088, 29092, 29095, 29099, 29103, 29106, 29110, 2862], 8798761794305677416223581583, 8798817837849271201303652243⟩
def ThetaRun14.s5 : Seg := ⟨8798761794305677416223581583, 8798817837849271201303652243, 477005529, 1048576, [29114, 29117, 29121, 29124, 29128, 29131, 29135, 29138, 29142, 29146, 29149, 29153, 29156, 29160, 29163, 29167, 29171, 29174, 29178, 29181, 29185, 29188, 29192, 29195, 29199, 29203, 29206, 29210, 29213, 29217, 29220, 29224, 29228, 29231, 29235, 27482], 8837509943821299246504843420, 8837566223645257073992227982⟩
def ThetaRun14.s6 : Seg := ⟨8837509943821299246504843420, 8837566223645257073992227982, 479102681, 1048576, [29242, 29245, 29249, 29252, 29256, 29259, 29263, 29267, 29270, 29274, 29277, 29281, 29284, 29288, 29292, 29295, 29299, 29302, 29306, 29310, 29313, 29317, 29320, 29324, 29327, 29331, 29335, 29338, 29342, 29345, 29349, 29352, 29356, 29360, 29363, 22993], 8876234124164724903958127990, 8876290639346505803082192935⟩
def ThetaRun14.s7 : Seg := ⟨8876234124164724903958127990, 8876290639346505803082192935, 481199833, 1048576, [29370, 29373, 29377, 29380, 29384, 29388, 29391, 29395, 29398, 29402, 29405, 29409, 29413, 29416, 29420, 29423, 29427, 29431, 29434, 29438, 29441, 29445, 29449, 29452, 29456, 29459, 29463, 29467, 29470, 29474, 29477, 29481, 29485, 29488, 29492, 18503], 8914935038753902117222759821, 8914991788669650431390651427⟩
def ThetaRun14.s8 : Seg := ⟨8914935038753902117222759821, 8914991788669650431390651427, 483296985, 1048576, [29498, 29501, 29505, 29508, 29512, 29516, 29519, 29523, 29526, 29530, 29534, 29537, 29541, 29544, 29548, 29552, 29555, 29559, 29562, 29566, 29570, 29573, 29577, 29581, 29584, 29588, 29591, 29595, 29599, 29602, 29606, 29609, 29613, 29617, 29620, 14015], 8953615579139884086654402535, 8953672563468736928136126944⟩
def ThetaRun14.s9 : Seg := ⟨8953615579139884086654402535, 8953672563468736928136126944, 485394137, 1048576, [29626, 29629, 29633, 29636, 29640, 29644, 29647, 29651, 29655, 29658, 29662, 29665, 29669, 29673, 29676, 29680, 29684, 29687, 29691, 29694, 29698, 29702, 29705, 29709, 29713, 29716, 29720, 29723, 29727, 29731, 29734, 29738, 29742, 29745, 29749, 9524], 8992287132440994855432586547, 8992344351317935535287810040⟩
def ThetaRun14.s10 : Seg := ⟨8992287132440994855432586547, 8992344351317935535287810040, 487491289, 1048576, [29754, 29757, 29761, 29765, 29768, 29772, 29775, 29779, 29783, 29786, 29790, 29794, 29797, 29801, 29804, 29808, 29812, 29815, 29819, 29823, 29826, 29830, 29834, 29837, 29841, 29845, 29848, 29852, 29855, 29859, 29863, 29866, 29870, 29874, 29877, 5036], 9030955563611039814538150136, 9031013017463967792825524120⟩
def ThetaRun14.s11 : Seg := ⟨9030955563611039814538150136, 9031013017463967792825524120, 489588441, 1048576, [29882, 29885, 29889, 29893, 29896, 29900, 29903, 29907, 29911, 29914, 29918, 29922, 29925, 29929, 29933, 29936, 29940, 29944, 29947, 29951, 29955, 29958, 29962, 29966, 29969, 29973, 29977, 29980, 29984, 29988, 29991, 29995, 29999, 30002, 30006, 546], 9069652571913404530436561480, 9069710261667207536755569806⟩
def ThetaRun14.s12 : Seg := ⟨9069652571913404530436561480, 9069710261667207536755569806, 491685593, 1048576, [30010, 30013, 30017, 30021, 30024, 30028, 30032, 30035, 30039, 30043, 30046, 30050, 30054, 30057, 30061, 30065, 30068, 30072, 30076, 30079, 30083, 30087, 30090, 30094, 30098, 30101, 30105, 30109, 30112, 30116, 30120, 30123, 30127, 30131, 26190], 9108310572481780851773615598, 9108368497211964993519832289⟩
def ThetaRun14.s13 : Seg := ⟨9108310572481780851773615598, 9108368497211964993519832289, 493782745, 1048576, [30138, 30141, 30145, 30149, 30152, 30156, 30160, 30163, 30167, 30171, 30174, 30178, 30182, 30185, 30189, 30193, 30197, 30200, 30204, 30208, 30211, 30215, 30219, 30222, 30226, 30230, 30233, 30237, 30241, 30244, 30248, 30252, 30256, 30259, 21831], 9147045832411465892888310391, 9147103991932194775797361277⟩
def ThetaRun14.s14 : Seg := ⟨9147045832411465892888310391, 9147103991932194775797361277, 495879897, 1048576, [30266, 30269, 30273, 30277, 30280, 30284, 30288, 30291, 30295, 30299, 30303, 30306, 30310, 30314, 30317, 30321, 30325, 30328, 30332, 30336, 30340, 30343, 30347, 30351, 30354, 30358, 30362, 30366, 30369, 30373, 30377, 30380, 30384, 30388, 17470], 9185749748563016755018826389, 9185808142367982037241505788⟩
def ThetaRun14.s15 : Seg := ⟨9185749748563016755018826389, 9185808142367982037241505788, 497977049, 1048576, [30394, 30397, 30401, 30405, 30408, 30412, 30416, 30420, 30423, 30427, 30431, 30434, 30438, 30442, 30446, 30449, 30453, 30457, 30460, 30464, 30468, 30472, 30475, 30479, 30483, 30486, 30490, 30494, 30498, 30501, 30505, 30509, 30513, 30516, 13110], 9224410454497629098516192387, 9224469082250828843885732126⟩
def ThetaRun14.s16 : Seg := ⟨9224410454497629098516192387, 9224469082250828843885732126, 500074201, 1048576, [30522, 30525, 30529, 30533, 30537, 30540, 30544, 30548, 30551, 30555, 30559, 30563, 30566, 30570, 30574, 30578, 30581, 30585, 30589, 30592, 30596, 30600, 30604, 30607, 30611, 30615, 30619, 30622, 30626, 30630, 30634, 30637, 30641, 30645, 8748], 9262999434495844298492694652, 9263058295987943978385050605⟩

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