Theta certificate data, block 6

Definition
ThetaCertData_6
by @bwdaugherty · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)
analytic-number-theorynumber-theoryprime-numbers
Certificate records, block 6 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_6 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 ThetaRun6.s0 : Seg := ⟨3344336131464228100347825928, 3344358267474907607021862388, 181307097, 1048576, [11066, 11067, 11068, 11070, 11071, 11072, 11074, 11075, 11076, 11078, 11079, 11080, 11082, 11083, 11085, 11086, 11087, 11089, 11090, 11091, 11093, 11094, 11095, 11097, 11098, 11099, 11101, 11102, 11103, 11105, 11106, 11108, 11109, 11110, 11112, 11113, 11114, 11116, 11117, 11118, 11120, 11121, 11122, 11124, 11125, 11127, 11128, 11129, 11131, 11132, 11133, 11135, 11136, 11137, 11139, 11140, 11142, 11143, 11144, 11146, 11147, 11148, 11150, 11151, 11152, 11154, 11155, 11156, 11158, 11159, 11161, 11162, 11163, 11165, 11166, 11167, 11169, 11170, 11171, 11173, 11174, 11176, 11177, 11178, 11180, 11181, 11182, 11184, 11185, 11186, 11188, 11189, 11191, 11192, 2483], 3382905182480608324213868561, 3382927565537771046458858871⟩
def ThetaRun6.s1 : Seg := ⟨3382905182480608324213868561, 3382927565537771046458858871, 183404249, 1048576, [11194, 11195, 11196, 11198, 11199, 11200, 11202, 11203, 11205, 11206, 11207, 11209, 11210, 11211, 11213, 11214, 11215, 11217, 11218, 11220, 11221, 11222, 11224, 11225, 11226, 11228, 11229, 11231, 11232, 11233, 11235, 11236, 11237, 11239, 11240, 11242, 11243, 11244, 11246, 11247, 11248, 11250, 11251, 11253, 11254, 11255, 11257, 11258, 11259, 11261, 11262, 11264, 11265, 11266, 11268, 11269, 11270, 11272, 11273, 11275, 11276, 11277, 11279, 11280, 11281, 11283, 11284, 11286, 11287, 11288, 11290, 11291, 11292, 11294, 11295, 11297, 11298, 11299, 11301, 11302, 11303, 11305, 11306, 11308, 11309, 11310, 11312, 11313, 11314, 11316, 11317, 11319, 11320, 1702], 3421715444764171899264615354, 3421738076371090321827184274⟩
def ThetaRun6.s2 : Seg := ⟨3421715444764171899264615354, 3421738076371090321827184274, 185501401, 1048576, [11322, 11323, 11324, 11326, 11327, 11329, 11330, 11331, 11333, 11334, 11335, 11337, 11338, 11340, 11341, 11342, 11344, 11345, 11347, 11348, 11349, 11351, 11352, 11353, 11355, 11356, 11358, 11359, 11360, 11362, 11363, 11365, 11366, 11367, 11369, 11370, 11371, 11373, 11374, 11376, 11377, 11378, 11380, 11381, 11383, 11384, 11385, 11387, 11388, 11390, 11391, 11392, 11394, 11395, 11396, 11398, 11399, 11401, 11402, 11403, 11405, 11406, 11408, 11409, 11410, 11412, 11413, 11415, 11416, 11417, 11419, 11420, 11422, 11423, 11424, 11426, 11427, 11429, 11430, 11431, 11433, 11434, 11435, 11437, 11438, 11440, 11441, 11442, 11444, 11445, 11447, 11448, 1181], 3460400522406722193133574152, 3460423401695254322879618722⟩
def ThetaRun6.s3 : Seg := ⟨3460400522406722193133574152, 3460423401695254322879618722, 187598553, 1048576, [11450, 11451, 11452, 11454, 11455, 11457, 11458, 11459, 11461, 11462, 11464, 11465, 11466, 11468, 11469, 11471, 11472, 11473, 11475, 11476, 11478, 11479, 11480, 11482, 11483, 11485, 11486, 11487, 11489, 11490, 11492, 11493, 11494, 11496, 11497, 11499, 11500, 11501, 11503, 11504, 11506, 11507, 11508, 11510, 11511, 11513, 11514, 11515, 11517, 11518, 11520, 11521, 11523, 11524, 11525, 11527, 11528, 11530, 11531, 11532, 11534, 11535, 11537, 11538, 11539, 11541, 11542, 11544, 11545, 11546, 11548, 11549, 11551, 11552, 11553, 11555, 11556, 11558, 11559, 11561, 11562, 11563, 11565, 11566, 11568, 11569, 11570, 11572, 11573, 11575, 11576, 918], 3499048895581303640853975094, 3499072022226113598432466740⟩
def ThetaRun6.s4 : Seg := ⟨3499048895581303640853975094, 3499072022226113598432466740, 189695705, 1048576, [11578, 11579, 11580, 11582, 11583, 11585, 11586, 11588, 11589, 11590, 11592, 11593, 11595, 11596, 11597, 11599, 11600, 11602, 11603, 11604, 11606, 11607, 11609, 11610, 11612, 11613, 11614, 11616, 11617, 11619, 11620, 11621, 11623, 11624, 11626, 11627, 11629, 11630, 11631, 11633, 11634, 11636, 11637, 11639, 11640, 11641, 11643, 11644, 11646, 11647, 11648, 11650, 11651, 11653, 11654, 11656, 11657, 11658, 11660, 11661, 11663, 11664, 11666, 11667, 11668, 11670, 11671, 11673, 11674, 11676, 11677, 11678, 11680, 11681, 11683, 11684, 11686, 11687, 11688, 11690, 11691, 11693, 11694, 11695, 11697, 11698, 11700, 11701, 11703, 11704, 911], 3537658126546101274555013121, 3537681500150930121695342740⟩
def ThetaRun6.s5 : Seg := ⟨3537658126546101274555013121, 3537681500150930121695342740, 191792857, 1048576, [11706, 11707, 11708, 11710, 11711, 11713, 11714, 11716, 11717, 11718, 11720, 11721, 11723, 11724, 11726, 11727, 11728, 11730, 11731, 11733, 11734, 11736, 11737, 11739, 11740, 11741, 11743, 11744, 11746, 11747, 11749, 11750, 11751, 11753, 11754, 11756, 11757, 11759, 11760, 11761, 11763, 11764, 11766, 11767, 11769, 11770, 11772, 11773, 11774, 11776, 11777, 11779, 11780, 11782, 11783, 11784, 11786, 11787, 11789, 11790, 11792, 11793, 11795, 11796, 11797, 11799, 11800, 11802, 11803, 11805, 11806, 11807, 11809, 11810, 11812, 11813, 11815, 11816, 11818, 11819, 11820, 11822, 11823, 11825, 11826, 11828, 11829, 11831, 11832, 1162], 3576384543822911506311937379, 3576408164945447666302801981⟩
def ThetaRun6.s6 : Seg := ⟨3576384543822911506311937379, 3576408164945447666302801981, 193890009, 1048576, [11834, 11835, 11836, 11838, 11839, 11841, 11842, 11844, 11845, 11847, 11848, 11850, 11851, 11852, 11854, 11855, 11857, 11858, 11860, 11861, 11863, 11864, 11865, 11867, 11868, 11870, 11871, 11873, 11874, 11876, 11877, 11878, 11880, 11881, 11883, 11884, 11886, 11887, 11889, 11890, 11892, 11893, 11894, 11896, 11897, 11899, 11900, 11902, 11903, 11905, 11906, 11908, 11909, 11910, 11912, 11913, 11915, 11916, 11918, 11919, 11921, 11922, 11924, 11925, 11926, 11928, 11929, 11931, 11932, 11934, 11935, 11937, 11938, 11940, 11941, 11942, 11944, 11945, 11947, 11948, 11950, 11951, 11953, 11954, 11956, 11957, 11958, 11960, 1668], 3615100157649565037343269231, 3615124025968688045150843089⟩
def ThetaRun6.s7 : Seg := ⟨3615100157649565037343269231, 3615124025968688045150843089, 195987161, 1048576, [11962, 11963, 11965, 11966, 11967, 11969, 11970, 11972, 11973, 11975, 11976, 11978, 11979, 11981, 11982, 11984, 11985, 11986, 11988, 11989, 11991, 11992, 11994, 11995, 11997, 11998, 12000, 12001, 12003, 12004, 12005, 12007, 12008, 12010, 12011, 12013, 12014, 12016, 12017, 12019, 12020, 12022, 12023, 12025, 12026, 12027, 12029, 12030, 12032, 12033, 12035, 12036, 12038, 12039, 12041, 12042, 12044, 12045, 12047, 12048, 12050, 12051, 12052, 12054, 12055, 12057, 12058, 12060, 12061, 12063, 12064, 12066, 12067, 12069, 12070, 12072, 12073, 12075, 12076, 12078, 12079, 12080, 12082, 12083, 12085, 12086, 12088, 2435], 3653655684318402584478688267, 3653679798606825872120236652⟩
def ThetaRun6.s8 : Seg := ⟨3653655684318402584478688267, 3653679798606825872120236652, 198084313, 1048576, [12090, 12091, 12093, 12094, 12096, 12097, 12098, 12100, 12101, 12103, 12104, 12106, 12107, 12109, 12110, 12112, 12113, 12115, 12116, 12118, 12119, 12121, 12122, 12124, 12125, 12127, 12128, 12130, 12131, 12132, 12134, 12135, 12137, 12138, 12140, 12141, 12143, 12144, 12146, 12147, 12149, 12150, 12152, 12153, 12155, 12156, 12158, 12159, 12161, 12162, 12164, 12165, 12167, 12168, 12170, 12171, 12173, 12174, 12176, 12177, 12178, 12180, 12181, 12183, 12184, 12186, 12187, 12189, 12190, 12192, 12193, 12195, 12196, 12198, 12199, 12201, 12202, 12204, 12205, 12207, 12208, 12210, 12211, 12213, 12214, 12216, 3457], 3692395453554736213349804710, 3692419814677617839731490285⟩
def ThetaRun6.s9 : Seg := ⟨3692395453554736213349804710, 3692419814677617839731490285, 200181465, 1048576, [12218, 12219, 12221, 12222, 12224, 12225, 12227, 12228, 12230, 12231, 12233, 12234, 12236, 12237, 12239, 12240, 12241, 12243, 12244, 12246, 12247, 12249, 12250, 12252, 12253, 12255, 12256, 12258, 12259, 12261, 12262, 12264, 12265, 12267, 12268, 12270, 12271, 12273, 12274, 12276, 12277, 12279, 12280, 12282, 12283, 12285, 12286, 12288, 12289, 12291, 12292, 12294, 12295, 12297, 12298, 12300, 12301, 12303, 12304, 12306, 12307, 12309, 12310, 12312, 12313, 12315, 12316, 12318, 12319, 12321, 12322, 12324, 12325, 12327, 12328, 12330, 12331, 12333, 12334, 12336, 12337, 12339, 12341, 12342, 12344, 4745], 3731059817895003428440287712, 3731084425153296828943752175⟩
def ThetaRun6.s10 : Seg := ⟨3731059817895003428440287712, 3731084425153296828943752175, 202278617, 1048576, [12346, 12347, 12349, 12350, 12352, 12353, 12355, 12356, 12358, 12359, 12361, 12362, 12364, 12365, 12367, 12368, 12370, 12371, 12373, 12374, 12376, 12377, 12379, 12380, 12382, 12383, 12385, 12386, 12388, 12389, 12391, 12392, 12394, 12395, 12397, 12398, 12400, 12401, 12403, 12405, 12406, 12408, 12409, 12411, 12412, 12414, 12415, 12417, 12418, 12420, 12421, 12423, 12424, 12426, 12427, 12429, 12430, 12432, 12433, 12435, 12436, 12438, 12439, 12441, 12442, 12444, 12445, 12447, 12449, 12450, 12452, 12453, 12455, 12456, 12458, 12459, 12461, 12462, 12464, 12465, 12467, 12468, 12470, 12471, 6273], 3769719029852467368470090105, 3769743883061112197759392483⟩
def ThetaRun6.s11 : Seg := ⟨3769719029852467368470090105, 3769743883061112197759392483, 204375769, 1048576, [12474, 12475, 12477, 12478, 12480, 12481, 12483, 12484, 12486, 12487, 12489, 12490, 12492, 12493, 12495, 12496, 12498, 12500, 12501, 12503, 12504, 12506, 12507, 12509, 12510, 12512, 12513, 12515, 12516, 12518, 12519, 12521, 12522, 12524, 12525, 12527, 12529, 12530, 12532, 12533, 12535, 12536, 12538, 12539, 12541, 12542, 12544, 12545, 12547, 12548, 12550, 12551, 12553, 12555, 12556, 12558, 12559, 12561, 12562, 12564, 12565, 12567, 12568, 12570, 12571, 12573, 12575, 12576, 12578, 12579, 12581, 12582, 12584, 12585, 12587, 12588, 12590, 12591, 12593, 12594, 12596, 12598, 12599, 8068], 3808428276835486551106039275, 3808453376226668400325249193⟩
def ThetaRun6.s12 : Seg := ⟨3808428276835486551106039275, 3808453376226668400325249193, 206472921, 1048576, [12602, 12603, 12605, 12606, 12608, 12609, 12611, 12612, 12614, 12615, 12617, 12619, 12620, 12622, 12623, 12625, 12626, 12628, 12629, 12631, 12632, 12634, 12635, 12637, 12639, 12640, 12642, 12643, 12645, 12646, 12648, 12649, 12651, 12652, 12654, 12656, 12657, 12659, 12660, 12662, 12663, 12665, 12666, 12668, 12669, 12671, 12673, 12674, 12676, 12677, 12679, 12680, 12682, 12683, 12685, 12686, 12688, 12690, 12691, 12693, 12694, 12696, 12697, 12699, 12700, 12702, 12704, 12705, 12707, 12708, 12710, 12711, 12713, 12714, 12716, 12718, 12719, 12721, 12722, 12724, 12725, 12727, 10119], 3847098005866212528527680642, 3847123351238113828469245143⟩
def ThetaRun6.s13 : Seg := ⟨3847098005866212528527680642, 3847123351238113828469245143, 208570073, 1048576, [12730, 12731, 12733, 12734, 12736, 12737, 12739, 12740, 12742, 12744, 12745, 12747, 12748, 12750, 12751, 12753, 12754, 12756, 12758, 12759, 12761, 12762, 12764, 12765, 12767, 12769, 12770, 12772, 12773, 12775, 12776, 12778, 12779, 12781, 12783, 12784, 12786, 12787, 12789, 12790, 12792, 12793, 12795, 12797, 12798, 12800, 12801, 12803, 12804, 12806, 12808, 12809, 12811, 12812, 12814, 12815, 12817, 12818, 12820, 12822, 12823, 12825, 12826, 12828, 12829, 12831, 12833, 12834, 12836, 12837, 12839, 12840, 12842, 12844, 12845, 12847, 12848, 12850, 12851, 12853, 12855, 12427], 3885807835227633719861724403, 3885833427095556202065779802⟩
def ThetaRun6.s14 : Seg := ⟨3885807835227633719861724403, 3885833427095556202065779802, 210667225, 1048576, [12858, 12859, 12861, 12862, 12864, 12865, 12867, 12869, 12870, 12872, 12873, 12875, 12876, 12878, 12880, 12881, 12883, 12884, 12886, 12887, 12889, 12891, 12892, 12894, 12895, 12897, 12898, 12900, 12902, 12903, 12905, 12906, 12908, 12910, 12911, 12913, 12914, 12916, 12917, 12919, 12921, 12922, 12924, 12925, 12927, 12928, 12930, 12932, 12933, 12935, 12936, 12938, 12939, 12941, 12943, 12944, 12946, 12947, 12949, 12951, 12952, 12954, 12955, 12957, 12958, 12960, 12962, 12963, 12965, 12966, 12968, 12970, 12971, 12973, 12974, 12976, 12977, 12979, 12981, 12982, 12984, 2008], 3924472358315951751502292651, 3924498196001690711619367570⟩
def ThetaRun6.s15 : Seg := ⟨3924472358315951751502292651, 3924498196001690711619367570, 212764377, 1048576, [12986, 12987, 12989, 12990, 12992, 12994, 12995, 12997, 12998, 13000, 13001, 13003, 13005, 13006, 13008, 13009, 13011, 13013, 13014, 13016, 13017, 13019, 13021, 13022, 13024, 13025, 13027, 13028, 13030, 13032, 13033, 13035, 13036, 13038, 13040, 13041, 13043, 13044, 13046, 13048, 13049, 13051, 13052, 13054, 13056, 13057, 13059, 13060, 13062, 13064, 13065, 13067, 13068, 13070, 13071, 13073, 13075, 13076, 13078, 13079, 13081, 13083, 13084, 13086, 13087, 13089, 13091, 13092, 13094, 13095, 13097, 13099, 13100, 13102, 13103, 13105, 13107, 13108, 13110, 13111, 4703], 3963162079166493860928729914, 3963188162355024871581506066⟩
def ThetaRun6.s16 : Seg := ⟨3963162079166493860928729914, 3963188162355024871581506066, 214861529, 1048576, [13114, 13115, 13117, 13118, 13120, 13122, 13123, 13125, 13126, 13128, 13130, 13131, 13133, 13134, 13136, 13138, 13139, 13141, 13142, 13144, 13146, 13147, 13149, 13150, 13152, 13154, 13155, 13157, 13159, 13160, 13162, 13163, 13165, 13167, 13168, 13170, 13171, 13173, 13175, 13176, 13178, 13179, 13181, 13183, 13184, 13186, 13187, 13189, 13191, 13192, 13194, 13195, 13197, 13199, 13200, 13202, 13204, 13205, 13207, 13208, 13210, 13212, 13213, 13215, 13216, 13218, 13220, 13221, 13223, 13225, 13226, 13228, 13229, 13231, 13233, 13234, 13236, 13237, 13239, 7654], 4001841733681926712131771836, 4001868062150770228487153761⟩

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