Theta certificate data, block 18

Definition

ThetaCertData_18

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

analytic-number-theorynumber-theoryprime-numbers

Certificate records, block 18 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_18 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 ThetaRun18.s0 : Seg := ⟨11235990050891527578941519695, 11236060808435352050237361380, 609126105, 1048576, [37178, 37182, 37187, 37191, 37196, 37200, 37205, 37209, 37214, 37218, 37223, 37228, 37232, 37237, 37241, 37246, 37250, 37255, 37259, 37264, 37268, 37273, 37278, 37282, 37287, 37291, 37296, 37300, 5886], 11274662026039514307605424286, 11274733015862819495225982153⟩
def ThetaRun18.s1 : Seg := ⟨11274662026039514307605424286, 11274733015862819495225982153, 611223257, 1048576, [37306, 37310, 37315, 37319, 37324, 37328, 37333, 37337, 37342, 37347, 37351, 37356, 37360, 37365, 37369, 37374, 37379, 37383, 37388, 37392, 37397, 37401, 37406, 37410, 37415, 37420, 37424, 37429, 2296], 11313433127556229432446559286, 11313504350776167534957055342⟩
def ThetaRun18.s2 : Seg := ⟨11313433127556229432446559286, 11313504350776167534957055342, 613320409, 1048576, [37434, 37438, 37443, 37447, 37452, 37456, 37461, 37466, 37470, 37475, 37479, 37484, 37488, 37493, 37498, 37502, 37507, 37511, 37516, 37521, 37525, 37530, 37534, 37539, 37543, 37548, 37553, 36263], 11352089834711095234950172130, 11352161290826678707701669021⟩
def ThetaRun18.s3 : Seg := ⟨11352089834711095234950172130, 11352161290826678707701669021, 615417561, 1048576, [37562, 37566, 37571, 37575, 37580, 37585, 37589, 37594, 37598, 37603, 37607, 37612, 37617, 37621, 37626, 37630, 37635, 37640, 37644, 37649, 37653, 37658, 37663, 37667, 37672, 37676, 37681, 32802], 11390636180914867211650021084, 11390707868574446429628333993⟩
def ThetaRun18.s4 : Seg := ⟨11390636180914867211650021084, 11390707868574446429628333993, 617514713, 1048576, [37690, 37694, 37699, 37703, 37708, 37713, 37717, 37722, 37726, 37731, 37736, 37740, 37745, 37749, 37754, 37759, 37763, 37768, 37773, 37777, 37782, 37786, 37791, 37796, 37800, 37805, 37809, 29340], 11429346214281462293864068724, 11429418133868095021610939570⟩
def ThetaRun18.s5 : Seg := ⟨11429346214281462293864068724, 11429418133868095021610939570, 619611865, 1048576, [37818, 37822, 37827, 37831, 37836, 37841, 37845, 37850, 37855, 37859, 37864, 37868, 37873, 37878, 37882, 37887, 37892, 37896, 37901, 37905, 37910, 37915, 37919, 37924, 37929, 37933, 37938, 25878], 11468020885931870143795176833, 11468093036882143074615254749⟩
def ThetaRun18.s6 : Seg := ⟨11468020885931870143795176833, 11468093036882143074615254749, 621709017, 1048576, [37946, 37950, 37955, 37960, 37964, 37969, 37973, 37978, 37983, 37987, 37992, 37997, 38001, 38006, 38011, 38015, 38020, 38024, 38029, 38034, 38038, 38043, 38048, 38052, 38057, 38062, 38066, 22416], 11506672865805742993286401245, 11506745247678397768745844510⟩
def ThetaRun18.s7 : Seg := ⟨11506672865805742993286401245, 11506745247678397768745844510, 623806169, 1048576, [38074, 38078, 38083, 38088, 38092, 38097, 38102, 38106, 38111, 38115, 38120, 38125, 38129, 38134, 38139, 38143, 38148, 38153, 38157, 38162, 38167, 38171, 38176, 38181, 38185, 38190, 38195, 18955], 11545370487555430865058204668, 11545443100527793621794590806⟩
def ThetaRun18.s8 : Seg := ⟨11545370487555430865058204668, 11545443100527793621794590806, 625903321, 1048576, [38202, 38206, 38211, 38216, 38220, 38225, 38230, 38234, 38239, 38244, 38248, 38253, 38258, 38262, 38267, 38272, 38276, 38281, 38286, 38290, 38295, 38300, 38304, 38309, 38314, 38318, 38323, 15493], 11584159715031368540213346652, 11584232559648856405947619328⟩
def ThetaRun18.s9 : Seg := ⟨11584159715031368540213346652, 11584232559648856405947619328, 628000473, 1048576, [38330, 38334, 38339, 38344, 38348, 38353, 38358, 38362, 38367, 38372, 38376, 38381, 38386, 38390, 38395, 38400, 38405, 38409, 38414, 38419, 38423, 38428, 38433, 38437, 38442, 38447, 38451, 12033], 11622820044120747366524277594, 11622893119841241915574020299⟩
def ThetaRun18.s10 : Seg := ⟨11622820044120747366524277594, 11622893119841241915574020299, 630097625, 1048576, [38458, 38462, 38467, 38472, 38476, 38481, 38486, 38490, 38495, 38500, 38505, 38509, 38514, 38519, 38523, 38528, 38533, 38537, 38542, 38547, 38552, 38556, 38561, 38566, 38570, 38575, 38580, 8572], 11661500554763636118264526327, 11661573861972999065764729881⟩
def ThetaRun18.s11 : Seg := ⟨11661500554763636118264526327, 11661573861972999065764729881, 632194777, 1048576, [38586, 38590, 38595, 38600, 38604, 38609, 38614, 38619, 38623, 38628, 38633, 38637, 38642, 38647, 38652, 38656, 38661, 38666, 38670, 38675, 38680, 38685, 38689, 38694, 38699, 38704, 38708, 5110], 11700110761027454415242812168, 11700184299805672551738870709⟩
def ThetaRun18.s12 : Seg := ⟨11700110761027454415242812168, 11700184299805672551738870709, 634291929, 1048576, [38714, 38718, 38723, 38728, 38733, 38737, 38742, 38747, 38751, 38756, 38761, 38766, 38770, 38775, 38780, 38785, 38789, 38794, 38799, 38803, 38808, 38813, 38818, 38822, 38827, 38832, 38837, 1648], 11738827473360965912731862318, 11738901244950497450627767807⟩
def ThetaRun18.s13 : Seg := ⟨11738827473360965912731862318, 11738901244950497450627767807, 636389081, 1048576, [38842, 38846, 38851, 38856, 38861, 38865, 38870, 38875, 38880, 38884, 38889, 38894, 38899, 38903, 38908, 38913, 38918, 38922, 38927, 38932, 38937, 38941, 38946, 38951, 38956, 38960, 37150], 11777547858984295031958794187, 11777621863322856807028853529⟩
def ThetaRun18.s14 : Seg := ⟨11777547858984295031958794187, 11777621863322856807028853529, 638486233, 1048576, [38970, 38974, 38979, 38984, 38989, 38993, 38998, 39003, 39008, 39012, 39017, 39022, 39027, 39031, 39036, 39041, 39046, 39051, 39055, 39060, 39065, 39070, 39074, 39079, 39084, 39089, 33819], 11816227021024389990537617887, 11816301257183262837669996779⟩
def ThetaRun18.s15 : Seg := ⟨11816227021024389990537617887, 11816301257183262837669996779, 640583385, 1048576, [39098, 39102, 39107, 39112, 39117, 39121, 39126, 39131, 39136, 39141, 39145, 39150, 39155, 39160, 39164, 39169, 39174, 39179, 39184, 39188, 39193, 39198, 39203, 39208, 39212, 39217, 30486], 11854916164792294612626913220, 11854990632308060393887612957⟩
def ThetaRun18.s16 : Seg := ⟨11854916164792294612626913220, 11854990632308060393887612957, 642680537, 1048576, [39226, 39230, 39235, 39240, 39245, 39250, 39254, 39259, 39264, 39269, 39274, 39278, 39283, 39288, 39293, 39297, 39302, 39307, 39312, 39317, 39321, 39326, 39331, 39336, 39341, 39345, 27153], 11893476093243748714394745165, 11893550790980782665606136059⟩

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