Theta certificate data, block 15

Definition

ThetaCertData_15

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

analytic-number-theorynumber-theoryprime-numbers

Certificate records, block 15 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_15 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 ThetaRun15.s0 : Seg := ⟨9262999434495844298492694652, 9263058295987943978385050605, 502171353, 1048576, [30650, 30653, 30657, 30661, 30665, 30668, 30672, 30676, 30680, 30683, 30687, 30691, 30695, 30698, 30702, 30706, 30710, 30713, 30717, 30721, 30725, 30728, 30732, 30736, 30740, 30743, 30747, 30751, 30755, 30758, 30762, 30766, 30770, 30773, 4385], 9301654863670114929346629818, 9301713959834296713800567914⟩
def ThetaRun15.s1 : Seg := ⟨9301654863670114929346629818, 9301713959834296713800567914, 504268505, 1048576, [30778, 30781, 30785, 30789, 30793, 30796, 30800, 30804, 30808, 30811, 30815, 30819, 30823, 30826, 30830, 30834, 30838, 30842, 30845, 30849, 30853, 30857, 30860, 30864, 30868, 30872, 30875, 30879, 30883, 30887, 30891, 30894, 30898, 30902, 27], 9340276911954570861966148549, 9340336243350587951291487951⟩
def ThetaRun15.s2 : Seg := ⟨9340276911954570861966148549, 9340336243350587951291487951, 506365657, 1048576, [30906, 30909, 30913, 30917, 30921, 30924, 30928, 30932, 30936, 30940, 30943, 30947, 30951, 30955, 30958, 30962, 30966, 30970, 30974, 30977, 30981, 30985, 30989, 30992, 30996, 31000, 31004, 31008, 31011, 31015, 31019, 31023, 31027, 26697], 9378926164322295065709146516, 9378985730233046481456288761⟩
def ThetaRun15.s3 : Seg := ⟨9378926164322295065709146516, 9378985730233046481456288761, 508462809, 1048576, [31034, 31037, 31041, 31045, 31049, 31053, 31056, 31060, 31064, 31068, 31072, 31075, 31079, 31083, 31087, 31090, 31094, 31098, 31102, 31106, 31109, 31113, 31117, 31121, 31125, 31128, 31132, 31136, 31140, 31144, 31147, 31151, 31155, 22465], 9417592982189115347032349170, 9417652782107289274164285913⟩
def ThetaRun15.s4 : Seg := ⟨9417592982189115347032349170, 9417652782107289274164285913, 510559961, 1048576, [31162, 31165, 31169, 31173, 31177, 31181, 31184, 31188, 31192, 31196, 31200, 31203, 31207, 31211, 31215, 31219, 31223, 31226, 31230, 31234, 31238, 31242, 31245, 31249, 31253, 31257, 31261, 31264, 31268, 31272, 31276, 31280, 31284, 18232], 9456245911106819107402790549, 9456305944576980202854712794⟩
def ThetaRun15.s5 : Seg := ⟨9456245911106819107402790549, 9456305944576980202854712794, 512657113, 1048576, [31290, 31293, 31297, 31301, 31305, 31309, 31313, 31316, 31320, 31324, 31328, 31332, 31335, 31339, 31343, 31347, 31351, 31355, 31358, 31362, 31366, 31370, 31374, 31378, 31381, 31385, 31389, 31393, 31397, 31401, 31404, 31408, 31412, 14000], 9494828276975195311680783479, 9494888543487442177286382519⟩
def ThetaRun15.s6 : Seg := ⟨9494828276975195311680783479, 9494888543487442177286382519, 514754265, 1048576, [31418, 31421, 31425, 31429, 31433, 31437, 31441, 31444, 31448, 31452, 31456, 31460, 31464, 31468, 31471, 31475, 31479, 31483, 31487, 31491, 31494, 31498, 31502, 31506, 31510, 31514, 31517, 31521, 31525, 31529, 31533, 31537, 31541, 9767], 9533557257992846072222656739, 9533617758674020679213927039⟩
def ThetaRun15.s7 : Seg := ⟨9533557257992846072222656739, 9533617758674020679213927039, 516851417, 1048576, [31546, 31549, 31553, 31557, 31561, 31565, 31569, 31573, 31576, 31580, 31584, 31588, 31592, 31596, 31600, 31603, 31607, 31611, 31615, 31619, 31623, 31627, 31630, 31634, 31638, 31642, 31646, 31650, 31654, 31657, 31661, 31665, 31669, 5536], 9572293697878535198766305176, 9572354433168199774601563138⟩
def ThetaRun15.s8 : Seg := ⟨9572293697878535198766305176, 9572354433168199774601563138, 518948569, 1048576, [31674, 31677, 31681, 31685, 31689, 31693, 31697, 31701, 31705, 31708, 31712, 31716, 31720, 31724, 31728, 31732, 31736, 31739, 31743, 31747, 31751, 31755, 31759, 31763, 31767, 31770, 31774, 31778, 31782, 31786, 31790, 31794, 31798, 1302], 9610962414118632954742972919, 9611023384290774509858670008⟩
def ThetaRun15.s9 : Seg := ⟨9610962414118632954742972919, 9611023384290774509858670008, 521045721, 1048576, [31802, 31805, 31809, 31813, 31817, 31821, 31825, 31829, 31833, 31837, 31840, 31844, 31848, 31852, 31856, 31860, 31864, 31868, 31872, 31875, 31879, 31883, 31887, 31891, 31895, 31899, 31903, 31907, 31910, 31914, 31918, 31922, 28998], 9649646669819062496023155272, 9649707874617685962634778267⟩
def ThetaRun15.s10 : Seg := ⟨9649646669819062496023155272, 9649707874617685962634778267, 523142873, 1048576, [31930, 31934, 31937, 31941, 31945, 31949, 31953, 31957, 31961, 31965, 31969, 31973, 31976, 31980, 31984, 31988, 31992, 31996, 32000, 32004, 32008, 32012, 32015, 32019, 32023, 32027, 32031, 32035, 32039, 32043, 32047, 32051, 24892], 9688329385936247209122691393, 9688390824671419880347011541⟩
def ThetaRun15.s11 : Seg := ⟨9688329385936247209122691393, 9688390824671419880347011541, 525240025, 1048576, [32058, 32062, 32065, 32069, 32073, 32077, 32081, 32085, 32089, 32093, 32097, 32101, 32105, 32109, 32112, 32116, 32120, 32124, 32128, 32132, 32136, 32140, 32144, 32148, 32152, 32156, 32160, 32163, 32167, 32171, 32175, 32179, 20789], 9727013872843339218215613808, 9727075545020506633781972188⟩
def ThetaRun15.s12 : Seg := ⟨9727013872843339218215613808, 9727075545020506633781972188, 527337177, 1048576, [32186, 32190, 32193, 32197, 32201, 32205, 32209, 32213, 32217, 32221, 32225, 32229, 32233, 32237, 32241, 32245, 32249, 32252, 32256, 32260, 32264, 32268, 32272, 32276, 32280, 32284, 32288, 32292, 32296, 32300, 32304, 32308, 16685], 9765730838588937488529588611, 9765792744241507450027780776⟩
def ThetaRun15.s13 : Seg := ⟨9765730838588937488529588611, 9765792744241507450027780776, 529434329, 1048576, [32314, 32318, 32321, 32325, 32329, 32333, 32337, 32341, 32345, 32349, 32353, 32357, 32361, 32365, 32369, 32373, 32377, 32381, 32385, 32389, 32393, 32397, 32400, 32404, 32408, 32412, 32416, 32420, 32424, 32428, 32432, 32436, 12584], 9804400222480142293368043630, 9804462361332018976615153423⟩
def ThetaRun15.s14 : Seg := ⟨9804400222480142293368043630, 9804462361332018976615153423, 531531481, 1048576, [32442, 32446, 32450, 32453, 32457, 32461, 32465, 32469, 32473, 32477, 32481, 32485, 32489, 32493, 32497, 32501, 32505, 32509, 32513, 32517, 32521, 32525, 32529, 32533, 32537, 32541, 32545, 32549, 32553, 32557, 32561, 32565, 8477], 9843109822762319576118894923, 9843172195349691246245524804⟩
def ThetaRun15.s15 : Seg := ⟨9843109822762319576118894923, 9843172195349691246245524804, 533628633, 1048576, [32570, 32574, 32578, 32582, 32586, 32589, 32593, 32597, 32601, 32605, 32609, 32613, 32617, 32621, 32625, 32629, 32633, 32637, 32641, 32645, 32649, 32653, 32657, 32661, 32665, 32669, 32673, 32677, 32681, 32685, 32689, 32693, 4379], 9881813278810715870086248287, 9881875885639828810775734747⟩
def ThetaRun15.s16 : Seg := ⟨9881813278810715870086248287, 9881875885639828810775734747, 535725785, 1048576, [32698, 32702, 32706, 32710, 32714, 32718, 32722, 32726, 32730, 32734, 32738, 32742, 32746, 32750, 32754, 32758, 32762, 32766, 32770, 32774, 32778, 32782, 32786, 32790, 32794, 32798, 32802, 32806, 32810, 32814, 32818, 32822, 256], 9920515369619301745083126349, 9920578211402761068659697488⟩

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