Theta certificate data, block 11

Definition

ThetaCertData_11

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

analytic-number-theorynumber-theoryprime-numbers

Certificate records, block 11 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_11 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 ThetaRun11.s0 : Seg := ⟨6632386913459139826346122861, 6632429689051493615425547943, 359565017, 1048576, [21946, 21948, 21951, 21954, 21956, 21959, 21962, 21964, 21967, 21970, 21972, 21975, 21978, 21980, 21983, 21986, 21989, 21991, 21994, 21997, 21999, 22002, 22005, 22007, 22010, 22013, 22015, 22018, 22021, 22023, 22026, 22029, 22031, 22034, 22037, 22040, 22042, 22045, 22048, 22050, 22053, 22056, 22058, 22061, 22064, 22066, 22069, 14232], 6670998468932722729631680944, 6671041482563901104054835466⟩
def ThetaRun11.s1 : Seg := ⟨6670998468932722729631680944, 6671041482563901104054835466, 361662169, 1048576, [22074, 22076, 22079, 22082, 22084, 22087, 22090, 22092, 22095, 22098, 22101, 22103, 22106, 22109, 22111, 22114, 22117, 22119, 22122, 22125, 22128, 22130, 22133, 22136, 22138, 22141, 22144, 22146, 22149, 22152, 22155, 22157, 22160, 22163, 22165, 22168, 22171, 22174, 22176, 22179, 22182, 22184, 22187, 22190, 22192, 22195, 22198, 8199], 6709712270245727138125303581, 6709755522413886901733975635⟩
def ThetaRun11.s2 : Seg := ⟨6709712270245727138125303581, 6709755522413886901733975635, 363759321, 1048576, [22202, 22204, 22207, 22210, 22212, 22215, 22218, 22221, 22223, 22226, 22229, 22231, 22234, 22237, 22240, 22242, 22245, 22248, 22250, 22253, 22256, 22259, 22261, 22264, 22267, 22269, 22272, 22275, 22278, 22280, 22283, 22286, 22288, 22291, 22294, 22297, 22299, 22302, 22305, 22308, 22310, 22313, 22316, 22318, 22321, 22324, 22327, 2166], 6748399212826826266201296050, 6748442704106114187385018202⟩
def ThetaRun11.s3 : Seg := ⟨6748399212826826266201296050, 6748442704106114187385018202, 365856473, 1048576, [22330, 22332, 22335, 22338, 22341, 22343, 22346, 22349, 22351, 22354, 22357, 22360, 22362, 22365, 22368, 22371, 22373, 22376, 22379, 22381, 22384, 22387, 22390, 22392, 22395, 22398, 22401, 22403, 22406, 22409, 22412, 22414, 22417, 22420, 22422, 22425, 22428, 22431, 22433, 22436, 22439, 22442, 22444, 22447, 22450, 22453, 18587], 6787127954294440724026811559, 6787171684564400311473012840⟩
def ThetaRun11.s4 : Seg := ⟨6787127954294440724026811559, 6787171684564400311473012840, 367953625, 1048576, [22458, 22460, 22463, 22466, 22469, 22471, 22474, 22477, 22480, 22482, 22485, 22488, 22491, 22493, 22496, 22499, 22502, 22504, 22507, 22510, 22512, 22515, 22518, 22521, 22523, 22526, 22529, 22532, 22534, 22537, 22540, 22543, 22545, 22548, 22551, 22554, 22557, 22559, 22562, 22565, 22568, 22570, 22573, 22576, 22579, 22581, 12683], 6825757275421197751587956874, 6825801243427824707693667767⟩
def ThetaRun11.s5 : Seg := ⟨6825757275421197751587956874, 6825801243427824707693667767, 370050777, 1048576, [22586, 22588, 22591, 22594, 22597, 22599, 22602, 22605, 22608, 22610, 22613, 22616, 22619, 22621, 22624, 22627, 22630, 22633, 22635, 22638, 22641, 22644, 22646, 22649, 22652, 22655, 22657, 22660, 22663, 22666, 22668, 22671, 22674, 22677, 22680, 22682, 22685, 22688, 22691, 22693, 22696, 22699, 22702, 22704, 22707, 22710, 6780], 6864385684425745887004610852, 6864429890286922541220837323⟩
def ThetaRun11.s6 : Seg := ⟨6864385684425745887004610852, 6864429890286922541220837323, 372147929, 1048576, [22714, 22716, 22719, 22722, 22725, 22727, 22730, 22733, 22736, 22739, 22741, 22744, 22747, 22750, 22752, 22755, 22758, 22761, 22764, 22766, 22769, 22772, 22775, 22777, 22780, 22783, 22786, 22789, 22791, 22794, 22797, 22800, 22803, 22805, 22808, 22811, 22814, 22816, 22819, 22822, 22825, 22828, 22830, 22833, 22836, 22839, 875], 6903037135276942108008721427, 6903081579967864741290069905⟩
def ThetaRun11.s7 : Seg := ⟨6903037135276942108008721427, 6903081579967864741290069905, 374245081, 1048576, [22842, 22844, 22847, 22850, 22853, 22856, 22858, 22861, 22864, 22867, 22870, 22872, 22875, 22878, 22881, 22883, 22886, 22889, 22892, 22895, 22897, 22900, 22903, 22906, 22909, 22911, 22914, 22917, 22920, 22923, 22925, 22928, 22931, 22934, 22937, 22939, 22942, 22945, 22948, 22951, 22953, 22956, 22959, 22962, 22965, 17938], 6941825195507652800236865464, 6941869879114775307805993367⟩
def ThetaRun11.s8 : Seg := ⟨6941825195507652800236865464, 6941869879114775307805993367, 376342233, 1048576, [22970, 22972, 22975, 22978, 22981, 22984, 22986, 22989, 22992, 22995, 22998, 23000, 23003, 23006, 23009, 23012, 23015, 23017, 23020, 23023, 23026, 23029, 23031, 23034, 23037, 23040, 23043, 23045, 23048, 23051, 23054, 23057, 23060, 23062, 23065, 23068, 23071, 23074, 23076, 23079, 23082, 23085, 23088, 23090, 23093, 12163], 6980666839407141427793548961, 6980711761783120215996801179⟩
def ThetaRun11.s9 : Seg := ⟨6980666839407141427793548961, 6980711761783120215996801179, 378439385, 1048576, [23098, 23100, 23103, 23106, 23109, 23112, 23115, 23117, 23120, 23123, 23126, 23129, 23131, 23134, 23137, 23140, 23143, 23146, 23148, 23151, 23154, 23157, 23160, 23163, 23165, 23168, 23171, 23174, 23177, 23180, 23182, 23185, 23188, 23191, 23194, 23196, 23199, 23202, 23205, 23208, 23211, 23213, 23216, 23219, 23222, 6388], 7019387109424630734088790532, 7019432270018609419140023114⟩
def ThetaRun11.s10 : Seg := ⟨7019387109424630734088790532, 7019432270018609419140023114, 380536537, 1048576, [23226, 23228, 23231, 23234, 23237, 23240, 23243, 23245, 23248, 23251, 23254, 23257, 23260, 23262, 23265, 23268, 23271, 23274, 23277, 23280, 23282, 23285, 23288, 23291, 23294, 23297, 23299, 23302, 23305, 23308, 23311, 23314, 23317, 23319, 23322, 23325, 23328, 23331, 23334, 23336, 23339, 23342, 23345, 23348, 23351, 612], 7058085366922202375708823701, 7058130766403227675593287342⟩
def ThetaRun11.s11 : Seg := ⟨7058085366922202375708823701, 7058130766403227675593287342, 382633689, 1048576, [23354, 23356, 23359, 23362, 23365, 23368, 23371, 23374, 23376, 23379, 23382, 23385, 23388, 23391, 23394, 23396, 23399, 23402, 23405, 23408, 23411, 23414, 23416, 23419, 23422, 23425, 23428, 23431, 23434, 23436, 23439, 23442, 23445, 23448, 23451, 23454, 23456, 23459, 23462, 23465, 23468, 23471, 23474, 23477, 18315], 7096706849283403869085752880, 7096752486345287136883875104⟩
def ThetaRun11.s12 : Seg := ⟨7096706849283403869085752880, 7096752486345287136883875104, 384730841, 1048576, [23482, 23484, 23487, 23490, 23493, 23496, 23499, 23502, 23505, 23507, 23510, 23513, 23516, 23519, 23522, 23525, 23528, 23530, 23533, 23536, 23539, 23542, 23545, 23548, 23550, 23553, 23556, 23559, 23562, 23565, 23568, 23571, 23574, 23576, 23579, 23582, 23585, 23588, 23591, 23594, 23597, 23599, 23602, 23605, 12669], 7135364150689397299317566267, 7135410025054035555571357300⟩
def ThetaRun11.s13 : Seg := ⟨7135364150689397299317566267, 7135410025054035555571357300, 386827993, 1048576, [23610, 23612, 23615, 23618, 23621, 23624, 23627, 23630, 23633, 23636, 23638, 23641, 23644, 23647, 23650, 23653, 23656, 23659, 23662, 23664, 23667, 23670, 23673, 23676, 23679, 23682, 23685, 23688, 23690, 23693, 23696, 23699, 23702, 23705, 23708, 23711, 23714, 23716, 23719, 23722, 23725, 23728, 23731, 23734, 7023], 7174071811540510915993223366, 7174117923639370916051187166⟩
def ThetaRun11.s14 : Seg := ⟨7174071811540510915993223366, 7174117923639370916051187166, 388925145, 1048576, [23738, 23741, 23743, 23746, 23749, 23752, 23755, 23758, 23761, 23764, 23767, 23770, 23772, 23775, 23778, 23781, 23784, 23787, 23790, 23793, 23796, 23799, 23801, 23804, 23807, 23810, 23813, 23816, 23819, 23822, 23825, 23828, 23831, 23833, 23836, 23839, 23842, 23845, 23848, 23851, 23854, 23857, 23860, 23863, 1373], 7212708290649106708140091928, 7212754640844072656579756369⟩
def ThetaRun11.s15 : Seg := ⟨7212708290649106708140091928, 7212754640844072656579756369, 391022297, 1048576, [23866, 23869, 23871, 23874, 23877, 23880, 23883, 23886, 23889, 23892, 23895, 23898, 23901, 23904, 23906, 23909, 23912, 23915, 23918, 23921, 23924, 23927, 23930, 23933, 23936, 23939, 23941, 23944, 23947, 23950, 23953, 23956, 23959, 23962, 23965, 23968, 23971, 23974, 23977, 23979, 23982, 23985, 23988, 19720], 7251424231330765601252576327, 7251470819568078671837485597⟩
def ThetaRun11.s16 : Seg := ⟨7251424231330765601252576327, 7251470819568078671837485597, 393119449, 1048576, [23994, 23997, 23999, 24002, 24005, 24008, 24011, 24014, 24017, 24020, 24023, 24026, 24029, 24032, 24035, 24038, 24041, 24043, 24046, 24049, 24052, 24055, 24058, 24061, 24064, 24067, 24070, 24073, 24076, 24079, 24082, 24085, 24088, 24090, 24093, 24096, 24099, 24102, 24105, 24108, 24111, 24114, 24117, 14202], 7290121049686207143020903770, 7290167875201571708472563419⟩

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