Theta certificate data, block 16

Definition

ThetaCertData_16

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

analytic-number-theorynumber-theoryprime-numbers

Certificate records, block 16 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_16 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 ThetaRun16.s0 : Seg := ⟨9920515369619301745083126349, 9920578211402761068659697488, 537822937, 1048576, [32826, 32830, 32834, 32838, 32842, 32846, 32850, 32854, 32858, 32862, 32866, 32870, 32874, 32878, 32882, 32886, 32890, 32894, 32898, 32902, 32906, 32910, 32914, 32918, 32922, 32926, 32930, 32934, 32938, 32942, 32946, 29110], 9959225711355605505402801845, 9959288787403849466528791984⟩
def ThetaRun16.s1 : Seg := ⟨9959225711355605505402801845, 9959288787403849466528791984, 539920089, 1048576, [32954, 32958, 32962, 32966, 32970, 32974, 32978, 32982, 32986, 32990, 32994, 32998, 33002, 33006, 33010, 33014, 33018, 33022, 33026, 33030, 33034, 33038, 33042, 33046, 33050, 33054, 33058, 33062, 33066, 33070, 33075, 25141], 9997874166040162676611927391, 9997937475350093111540711761⟩
def ThetaRun16.s2 : Seg := ⟨9997874166040162676611927391, 9997937475350093111540711761, 542017241, 1048576, [33082, 33086, 33090, 33094, 33098, 33102, 33106, 33110, 33114, 33118, 33122, 33126, 33130, 33134, 33138, 33142, 33146, 33150, 33154, 33158, 33162, 33167, 33171, 33175, 33179, 33183, 33187, 33191, 33195, 33199, 33203, 21164], 10036472551584915627628531199, 10036536093454857029905744533⟩
def ThetaRun16.s3 : Seg := ⟨10036472551584915627628531199, 10036536093454857029905744533, 544114393, 1048576, [33210, 33214, 33218, 33222, 33226, 33230, 33234, 33238, 33242, 33246, 33250, 33254, 33258, 33262, 33266, 33270, 33275, 33279, 33283, 33287, 33291, 33295, 33299, 33303, 33307, 33311, 33315, 33319, 33323, 33327, 33331, 17191], 10075152921670323453580743155, 10075216696413416444471076845⟩
def ThetaRun16.s4 : Seg := ⟨10075152921670323453580743155, 10075216696413416444471076845, 546211545, 1048576, [33338, 33342, 33346, 33350, 33354, 33358, 33362, 33366, 33370, 33374, 33378, 33382, 33386, 33391, 33395, 33399, 33403, 33407, 33411, 33415, 33419, 33423, 33427, 33431, 33435, 33439, 33444, 33448, 33452, 33456, 33460, 13215], 10113897092375875668973174186, 10113961100355552153503392328⟩
def ThetaRun16.s5 : Seg := ⟨10113897092375875668973174186, 10113961100355552153503392328, 548308697, 1048576, [33466, 33470, 33474, 33478, 33482, 33486, 33490, 33494, 33498, 33502, 33506, 33511, 33515, 33519, 33523, 33527, 33531, 33535, 33539, 33543, 33547, 33552, 33556, 33560, 33564, 33568, 33572, 33576, 33580, 33584, 33588, 9240], 10152624128171765802844448860, 10152688369573631828653971708⟩
def ThetaRun16.s6 : Seg := ⟨10152624128171765802844448860, 10152688369573631828653971708, 550405849, 1048576, [33594, 33598, 33602, 33606, 33610, 33614, 33618, 33622, 33626, 33631, 33635, 33639, 33643, 33647, 33651, 33655, 33659, 33663, 33667, 33672, 33676, 33680, 33684, 33688, 33692, 33696, 33700, 33705, 33709, 33713, 33717, 5264], 10191371858383969022875072026, 10191436333754501594444512790⟩
def ThetaRun16.s7 : Seg := ⟨10191371858383969022875072026, 10191436333754501594444512790, 552503001, 1048576, [33722, 33726, 33730, 33734, 33738, 33742, 33746, 33750, 33755, 33759, 33763, 33767, 33771, 33775, 33779, 33783, 33788, 33792, 33796, 33800, 33804, 33808, 33812, 33816, 33821, 33825, 33829, 33833, 33837, 33841, 33845, 1289], 10230045558509765377546669537, 10230110268107295826315243444⟩
def ThetaRun16.s8 : Seg := ⟨10230045558509765377546669537, 10230110268107295826315243444, 554600153, 1048576, [33850, 33854, 33858, 33862, 33866, 33870, 33874, 33879, 33883, 33887, 33891, 33895, 33899, 33903, 33908, 33912, 33916, 33920, 33924, 33928, 33932, 33936, 33941, 33945, 33949, 33953, 33957, 33961, 33965, 33970, 31288], 10268743616340007541415635995, 10268808559968791784792114785⟩
def ThetaRun16.s9 : Seg := ⟨10268743616340007541415635995, 10268808559968791784792114785, 556697305, 1048576, [33978, 33982, 33986, 33990, 33994, 33998, 34003, 34007, 34011, 34015, 34019, 34023, 34027, 34032, 34036, 34040, 34044, 34048, 34052, 34056, 34061, 34065, 34069, 34073, 34077, 34081, 34086, 34090, 34094, 34098, 27441], 10307411765623390272158110450, 10307476942405451384654775217⟩
def ThetaRun16.s10 : Seg := ⟨10307411765623390272158110450, 10307476942405451384654775217, 558794457, 1048576, [34106, 34110, 34114, 34118, 34122, 34126, 34131, 34135, 34139, 34143, 34147, 34151, 34156, 34160, 34164, 34168, 34172, 34176, 34181, 34185, 34189, 34193, 34197, 34201, 34206, 34210, 34214, 34218, 34222, 34227, 23595], 10346093066550124926690144451, 10346158476087111671433911220⟩
def ThetaRun16.s11 : Seg := ⟨10346093066550124926690144451, 10346158476087111671433911220, 560891609, 1048576, [34234, 34238, 34242, 34246, 34250, 34255, 34259, 34263, 34267, 34271, 34275, 34280, 34284, 34288, 34292, 34296, 34301, 34305, 34309, 34313, 34317, 34321, 34326, 34330, 34334, 34338, 34342, 34347, 34351, 34355, 19747], 10384788983871795497586302519, 10384854625950196941974070144⟩
def ThetaRun16.s12 : Seg := ⟨10384788983871795497586302519, 10384854625950196941974070144, 562988761, 1048576, [34362, 34366, 34370, 34374, 34378, 34383, 34387, 34391, 34395, 34399, 34404, 34408, 34412, 34416, 34420, 34425, 34429, 34433, 34437, 34441, 34446, 34450, 34454, 34458, 34462, 34467, 34471, 34475, 34479, 34483, 15901], 10423445216184912767707069203, 10423511090456982753301199481⟩
def ThetaRun16.s13 : Seg := ⟨10423445216184912767707069203, 10423511090456982753301199481, 565085913, 1048576, [34490, 34494, 34498, 34502, 34506, 34511, 34515, 34519, 34523, 34528, 34532, 34536, 34540, 34544, 34549, 34553, 34557, 34561, 34565, 34570, 34574, 34578, 34582, 34587, 34591, 34595, 34599, 34603, 34608, 34612, 12054], 10462131618580404463092331247, 10462197725359981269859177212⟩
def ThetaRun16.s14 : Seg := ⟨10462131618580404463092331247, 10462197725359981269859177212, 567183065, 1048576, [34618, 34622, 34626, 34630, 34635, 34639, 34643, 34647, 34651, 34656, 34660, 34664, 34668, 34673, 34677, 34681, 34685, 34690, 34694, 34698, 34702, 34706, 34711, 34715, 34719, 34723, 34728, 34732, 34736, 34740, 8207], 10500826978551988065057929536, 10500893318225426909977526065⟩
def ThetaRun16.s15 : Seg := ⟨10500826978551988065057929536, 10500893318225426909977526065, 569280217, 1048576, [34746, 34750, 34754, 34758, 34763, 34767, 34771, 34775, 34780, 34784, 34788, 34792, 34797, 34801, 34805, 34809, 34814, 34818, 34822, 34826, 34831, 34835, 34839, 34843, 34848, 34852, 34856, 34860, 34865, 34869, 4358], 10539458001813018960826218958, 10539524574475287806887899598⟩
def ThetaRun16.s16 : Seg := ⟨10539458001813018960826218958, 10539524574475287806887899598, 571377369, 1048576, [34874, 34878, 34882, 34886, 34891, 34895, 34899, 34903, 34908, 34912, 34916, 34920, 34925, 34929, 34933, 34938, 34942, 34946, 34950, 34955, 34959, 34963, 34967, 34972, 34976, 34980, 34984, 34989, 34993, 34997, 514], 10578186078260511269898048414, 10578252885218007784841028224⟩

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