Theta certificate data, block 20

Definition

ThetaCertData_20

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

analytic-number-theorynumber-theoryprime-numbers

Certificate records, block 20 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_20 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 ThetaRun20.s0 : Seg := ⟨12551178427493398035010831113, 12551257049160436331183919394, 680429273, 1048576, [41530, 41535, 41540, 41545, 41550, 41555, 41560, 41565, 41570, 41575, 41580, 41585, 41590, 41596, 41601, 41606, 41611, 41616, 41621, 41626, 41631, 41636, 41641, 41646, 41651, 8814], 12589784787179466575318046862, 12589863638959146318388114804⟩
def ThetaRun20.s1 : Seg := ⟨12589784787179466575318046862, 12589863638959146318388114804, 682526425, 1048576, [41658, 41663, 41668, 41673, 41678, 41683, 41688, 41693, 41698, 41703, 41708, 41714, 41719, 41724, 41729, 41734, 41739, 41744, 41749, 41754, 41759, 41765, 41770, 41775, 41780, 5608], 12628472032928038080433113462, 12628551115729082267075402412⟩
def ThetaRun20.s2 : Seg := ⟨12628472032928038080433113462, 12628551115729082267075402412, 684623577, 1048576, [41786, 41791, 41796, 41801, 41806, 41811, 41816, 41821, 41826, 41832, 41837, 41842, 41847, 41852, 41857, 41862, 41867, 41872, 41878, 41883, 41888, 41893, 41898, 41903, 41908, 2403], 12667220644116742602129230530, 12667299958861504448709655844⟩
def ThetaRun20.s3 : Seg := ⟨12667220644116742602129230530, 12667299958861504448709655844, 686720729, 1048576, [41914, 41919, 41924, 41929, 41934, 41939, 41944, 41949, 41955, 41960, 41965, 41970, 41975, 41980, 41985, 41990, 41996, 42001, 42006, 42011, 42016, 42021, 42026, 42031, 41236], 12705936030135036147206929653, 12706015576939047355619954021⟩
def ThetaRun20.s4 : Seg := ⟨12705936030135036147206929653, 12706015576939047355619954021, 688817881, 1048576, [42042, 42047, 42052, 42057, 42062, 42067, 42072, 42078, 42083, 42088, 42093, 42098, 42103, 42108, 42114, 42119, 42124, 42129, 42134, 42139, 42144, 42150, 42155, 42160, 38158], 12744728168993577541726003517, 12744807947642992250097344646⟩
def ThetaRun20.s5 : Seg := ⟨12744728168993577541726003517, 12744807947642992250097344646, 690915033, 1048576, [42170, 42175, 42180, 42185, 42190, 42195, 42201, 42206, 42211, 42216, 42221, 42226, 42231, 42237, 42242, 42247, 42252, 42257, 42262, 42268, 42273, 42278, 42283, 42288, 35082], 12783332338833757598041042201, 12783412347686830925404469928⟩
def ThetaRun20.s6 : Seg := ⟨12783332338833757598041042201, 12783412347686830925404469928, 693012185, 1048576, [42298, 42303, 42308, 42313, 42318, 42323, 42329, 42334, 42339, 42344, 42349, 42354, 42360, 42365, 42370, 42375, 42380, 42385, 42391, 42396, 42401, 42406, 42411, 42417, 32007], 12822074071306028645357467255, 12822154310686298226660262023⟩
def ThetaRun20.s7 : Seg := ⟨12822074071306028645357467255, 12822154310686298226660262023, 695109337, 1048576, [42426, 42431, 42436, 42441, 42446, 42452, 42457, 42462, 42467, 42472, 42477, 42483, 42488, 42493, 42498, 42503, 42509, 42514, 42519, 42524, 42529, 42534, 42540, 42545, 28930], 12860799753940118408887585671, 12860880223407044545593822648⟩
def ThetaRun20.s8 : Seg := ⟨12860799753940118408887585671, 12860880223407044545593822648, 697206489, 1048576, [42554, 42559, 42564, 42569, 42574, 42580, 42585, 42590, 42595, 42600, 42606, 42611, 42616, 42621, 42626, 42632, 42637, 42642, 42647, 42652, 42658, 42663, 42668, 42673, 25854], 12899421850646012317368003717, 12899502549346712637290364947⟩
def ThetaRun20.s9 : Seg := ⟨12899421850646012317368003717, 12899502549346712637290364947, 699303641, 1048576, [42682, 42687, 42692, 42697, 42702, 42708, 42713, 42718, 42723, 42729, 42734, 42739, 42744, 42749, 42755, 42760, 42765, 42770, 42775, 42781, 42786, 42791, 42796, 42802, 22778], 12938121018194824407221857275, 12938201946455905632517899084⟩
def ThetaRun20.s10 : Seg := ⟨12938121018194824407221857275, 12938201946455905632517899084, 701400793, 1048576, [42810, 42815, 42820, 42825, 42831, 42836, 42841, 42846, 42851, 42857, 42862, 42867, 42872, 42878, 42883, 42888, 42893, 42899, 42904, 42909, 42914, 42919, 42925, 42930, 19701], 12976805946990231780840567034, 12976887104669123185021926076⟩
def ThetaRun20.s11 : Seg := ⟨12976805946990231780840567034, 12976887104669123185021926076, 703497945, 1048576, [42938, 42943, 42948, 42953, 42959, 42964, 42969, 42974, 42980, 42985, 42990, 42995, 43001, 43006, 43011, 43016, 43022, 43027, 43032, 43037, 43043, 43048, 43053, 43058, 16624], 13015507437285379754890732250, 13015588824548853105887426995⟩
def ThetaRun20.s12 : Seg := ⟨13015507437285379754890732250, 13015588824548853105887426995, 705595097, 1048576, [43066, 43071, 43076, 43081, 43087, 43092, 43097, 43102, 43108, 43113, 43118, 43123, 43129, 43134, 43139, 43145, 43150, 43155, 43160, 43166, 43171, 43176, 43181, 43187, 13549], 13054198790087603449782496356, 13054280407050101207912785149⟩
def ThetaRun20.s13 : Seg := ⟨13054198790087603449782496356, 13054280407050101207912785149, 707692249, 1048576, [43194, 43199, 43204, 43209, 43215, 43220, 43225, 43231, 43236, 43241, 43246, 43252, 43257, 43262, 43267, 43273, 43278, 43283, 43289, 43294, 43299, 43304, 43310, 43315, 10473], 13092884112013089274215926176, 13092965958953538198132444416⟩
def ThetaRun20.s14 : Seg := ⟨13092884112013089274215926176, 13092965958953538198132444416, 709789401, 1048576, [43322, 43327, 43332, 43337, 43343, 43348, 43353, 43359, 43364, 43369, 43375, 43380, 43385, 43390, 43396, 43401, 43406, 43412, 43417, 43422, 43427, 43433, 43438, 43443, 7397], 13131525414611793976006106208, 13131607491585292301583539160⟩
def ThetaRun20.s15 : Seg := ⟨13131525414611793976006106208, 13131607491585292301583539160, 711886553, 1048576, [43450, 43455, 43460, 43466, 43471, 43476, 43481, 43487, 43492, 43497, 43503, 43508, 43513, 43519, 43524, 43529, 43535, 43540, 43545, 43550, 43556, 43561, 43566, 43572, 4320], 13170209522328642578694957317, 13170291830079032686959473000⟩
def ThetaRun20.s16 : Seg := ⟨13170209522328642578694957317, 13170291830079032686959473000, 713983705, 1048576, [43578, 43583, 43588, 43594, 43599, 43604, 43610, 43615, 43620, 43626, 43631, 43636, 43641, 43647, 43652, 43657, 43663, 43668, 43673, 43679, 43684, 43689, 43695, 43700, 1244], 13208825870685764433987049777, 13208908409332243536794646682⟩

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