Theta certificate data, block 12

Definition

ThetaCertData_12

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

analytic-number-theorynumber-theoryprime-numbers

Certificate records, block 12 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_12 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 ThetaRun12.s0 : Seg := ⟨7290121049686207143020903770, 7290167875201571708472563419, 395216601, 1048576, [24122, 24125, 24127, 24130, 24133, 24136, 24139, 24142, 24145, 24148, 24151, 24154, 24157, 24160, 24163, 24166, 24169, 24172, 24175, 24178, 24181, 24184, 24186, 24189, 24192, 24195, 24198, 24201, 24204, 24207, 24210, 24213, 24216, 24219, 24222, 24225, 24228, 24231, 24234, 24237, 24240, 24243, 24246, 8683], 7328730728204457030844918219, 7328777790509296642238571112⟩
def ThetaRun12.s1 : Seg := ⟨7328730728204457030844918219, 7328777790509296642238571112, 397313753, 1048576, [24250, 24253, 24256, 24258, 24261, 24264, 24267, 24270, 24273, 24276, 24279, 24282, 24285, 24288, 24291, 24294, 24297, 24300, 24303, 24306, 24309, 24312, 24315, 24318, 24321, 24324, 24327, 24330, 24333, 24336, 24339, 24342, 24345, 24347, 24350, 24353, 24356, 24359, 24362, 24365, 24368, 24371, 24374, 3167], 7367403296158432358001332028, 7367450596199713842185751577⟩
def ThetaRun12.s2 : Seg := ⟨7367403296158432358001332028, 7367450596199713842185751577, 399410905, 1048576, [24378, 24381, 24384, 24387, 24390, 24392, 24395, 24398, 24401, 24404, 24407, 24410, 24413, 24416, 24419, 24422, 24425, 24428, 24431, 24434, 24437, 24440, 24443, 24446, 24449, 24452, 24455, 24458, 24461, 24464, 24467, 24470, 24473, 24476, 24479, 24482, 24485, 24488, 24491, 24494, 24497, 24500, 22154], 7406088669656661463123786701, 7406136207592079788953454054⟩
def ThetaRun12.s3 : Seg := ⟨7406088669656661463123786701, 7406136207592079788953454054, 401508057, 1048576, [24506, 24509, 24512, 24515, 24518, 24521, 24524, 24527, 24530, 24533, 24536, 24539, 24542, 24545, 24548, 24551, 24554, 24557, 24560, 24563, 24566, 24569, 24572, 24575, 24578, 24581, 24584, 24587, 24590, 24593, 24596, 24599, 24602, 24605, 24608, 24611, 24614, 24617, 24620, 24623, 24626, 24629, 16741], 7444809470643484635598651648, 7444857245951368951650376640⟩
def ThetaRun12.s4 : Seg := ⟨7444809470643484635598651648, 7444857245951368951650376640, 403605209, 1048576, [24634, 24637, 24640, 24643, 24646, 24649, 24652, 24655, 24658, 24661, 24664, 24667, 24670, 24673, 24676, 24679, 24682, 24685, 24688, 24691, 24694, 24697, 24700, 24703, 24706, 24709, 24712, 24715, 24718, 24721, 24724, 24727, 24730, 24733, 24736, 24739, 24742, 24745, 24748, 24751, 24754, 24757, 11365], 7483502773424016331401157205, 7483550785660873041127892454⟩
def ThetaRun12.s5 : Seg := ⟨7483502773424016331401157205, 7483550785660873041127892454, 405702361, 1048576, [24762, 24765, 24768, 24771, 24774, 24777, 24780, 24783, 24786, 24789, 24792, 24795, 24798, 24801, 24804, 24807, 24810, 24813, 24816, 24819, 24822, 24825, 24828, 24831, 24834, 24837, 24840, 24843, 24846, 24849, 24852, 24855, 24859, 24862, 24865, 24868, 24871, 24874, 24877, 24880, 24883, 24886, 5979], 7522189341246551193140584918, 7522237590661223721359141126⟩
def ThetaRun12.s6 : Seg := ⟨7522189341246551193140584918, 7522237590661223721359141126, 407799513, 1048576, [24890, 24893, 24896, 24899, 24902, 24905, 24908, 24911, 24914, 24917, 24920, 24923, 24926, 24929, 24932, 24935, 24938, 24941, 24944, 24947, 24950, 24953, 24957, 24960, 24963, 24966, 24969, 24972, 24975, 24978, 24981, 24984, 24987, 24990, 24993, 24996, 24999, 25002, 25005, 25008, 25011, 25014, 593], 7560836937664312059928265032, 7560885424870334645397940870⟩
def ThetaRun12.s7 : Seg := ⟨7560836937664312059928265032, 7560885424870334645397940870, 409896665, 1048576, [25018, 25021, 25024, 25027, 25030, 25033, 25036, 25039, 25042, 25045, 25048, 25051, 25054, 25057, 25060, 25063, 25067, 25070, 25073, 25076, 25079, 25082, 25085, 25088, 25091, 25094, 25097, 25100, 25103, 25106, 25109, 25112, 25116, 25119, 25122, 25125, 25128, 25131, 25134, 25137, 25140, 20344], 7599533284172684093611537041, 7599582008638334367948033060⟩
def ThetaRun12.s8 : Seg := ⟨7599533284172684093611537041, 7599582008638334367948033060, 411993817, 1048576, [25146, 25149, 25152, 25155, 25158, 25161, 25164, 25167, 25170, 25173, 25176, 25179, 25182, 25186, 25189, 25192, 25195, 25198, 25201, 25204, 25207, 25210, 25213, 25216, 25219, 25222, 25226, 25229, 25232, 25235, 25238, 25241, 25244, 25247, 25250, 25253, 25256, 25259, 25263, 25266, 25269, 15084], 7638227856301778955347563626, 7638276817444726871665096948⟩
def ThetaRun12.s9 : Seg := ⟨7638227856301778955347563626, 7638276817444726871665096948, 414090969, 1048576, [25274, 25277, 25280, 25283, 25286, 25289, 25292, 25295, 25298, 25301, 25304, 25308, 25311, 25314, 25317, 25320, 25323, 25326, 25329, 25332, 25335, 25338, 25342, 25345, 25348, 25351, 25354, 25357, 25360, 25363, 25366, 25369, 25373, 25376, 25379, 25382, 25385, 25388, 25391, 25394, 25397, 9824], 7676906308567451620089215933, 7676955506248462631817391429⟩
def ThetaRun12.s10 : Seg := ⟨7676906308567451620089215933, 7676955506248462631817391429, 416188121, 1048576, [25402, 25405, 25408, 25411, 25414, 25417, 25420, 25423, 25426, 25430, 25433, 25436, 25439, 25442, 25445, 25448, 25451, 25454, 25457, 25461, 25464, 25467, 25470, 25473, 25476, 25479, 25482, 25485, 25489, 25492, 25495, 25498, 25501, 25504, 25507, 25510, 25513, 25517, 25520, 25523, 25526, 4563], 7715624973018118390531496922, 7715674407968181046480027147⟩
def ThetaRun12.s11 : Seg := ⟨7715624973018118390531496922, 7715674407968181046480027147, 418285273, 1048576, [25530, 25533, 25536, 25539, 25542, 25545, 25548, 25551, 25555, 25558, 25561, 25564, 25567, 25570, 25573, 25576, 25580, 25583, 25586, 25589, 25592, 25595, 25598, 25601, 25605, 25608, 25611, 25614, 25617, 25620, 25623, 25626, 25630, 25633, 25636, 25639, 25642, 25645, 25648, 25651, 24956], 7754193006848971268933285444, 7754242678756955301773297532⟩
def ThetaRun12.s12 : Seg := ⟨7754193006848971268933285444, 7754242678756955301773297532, 420382425, 1048576, [25658, 25661, 25664, 25667, 25670, 25673, 25676, 25680, 25683, 25686, 25689, 25692, 25695, 25698, 25701, 25705, 25708, 25711, 25714, 25717, 25720, 25723, 25727, 25730, 25733, 25736, 25739, 25742, 25745, 25749, 25752, 25755, 25758, 25761, 25764, 25767, 25771, 25774, 25777, 25780, 19825], 7792910302640443732358043543, 7792960211449826385343937801⟩
def ThetaRun12.s13 : Seg := ⟨7792910302640443732358043543, 7792960211449826385343937801, 422479577, 1048576, [25786, 25789, 25792, 25795, 25798, 25801, 25804, 25808, 25811, 25814, 25817, 25820, 25823, 25827, 25830, 25833, 25836, 25839, 25842, 25845, 25849, 25852, 25855, 25858, 25861, 25864, 25868, 25871, 25874, 25877, 25880, 25883, 25887, 25890, 25893, 25896, 25899, 25902, 25905, 25909, 14693], 7831647176418206690523620539, 7831697321813693602887008130⟩
def ThetaRun12.s14 : Seg := ⟨7831647176418206690523620539, 7831697321813693602887008130, 424576729, 1048576, [25914, 25917, 25920, 25923, 25926, 25929, 25933, 25936, 25939, 25942, 25945, 25948, 25952, 25955, 25958, 25961, 25964, 25967, 25971, 25974, 25977, 25980, 25983, 25986, 25990, 25993, 25996, 25999, 26002, 26005, 26009, 26012, 26015, 26018, 26021, 26025, 26028, 26031, 26034, 26037, 9561], 7870380479711342826897540595, 7870430861679143008028367322⟩
def ThetaRun12.s15 : Seg := ⟨7870380479711342826897540595, 7870430861679143008028367322, 426673881, 1048576, [26042, 26045, 26048, 26051, 26054, 26058, 26061, 26064, 26067, 26070, 26073, 26077, 26080, 26083, 26086, 26089, 26093, 26096, 26099, 26102, 26105, 26108, 26112, 26115, 26118, 26121, 26124, 26128, 26131, 26134, 26137, 26140, 26144, 26147, 26150, 26153, 26156, 26159, 26163, 26166, 4427], 7909080852257764050721920535, 7909131471058634203628371765⟩
def ThetaRun12.s16 : Seg := ⟨7909080852257764050721920535, 7909131471058634203628371765, 428771033, 1048576, [26170, 26173, 26176, 26179, 26182, 26186, 26189, 26192, 26195, 26198, 26202, 26205, 26208, 26211, 26214, 26218, 26221, 26224, 26227, 26230, 26234, 26237, 26240, 26243, 26246, 26250, 26253, 26256, 26259, 26262, 26266, 26269, 26272, 26275, 26278, 26282, 26285, 26288, 26291, 25590], 7947694300911199595929133541, 7947745156654584578230695874⟩

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