Theta certificate data, block 21

Definition

ThetaCertData_21

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

analytic-number-theorynumber-theoryprime-numbers

Certificate records, block 21 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_21 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 ThetaRun21.s0 : Seg := ⟨13208825870685764433987049777, 13208908409332243536794646682, 716080857, 1048576, [43706, 43711, 43716, 43722, 43727, 43732, 43738, 43743, 43748, 43754, 43759, 43764, 43770, 43775, 43780, 43786, 43791, 43796, 43802, 43807, 43812, 43818, 43823, 41996], 13247533154193127024751519153, 13247615924161154082554902193⟩
def ThetaRun21.s1 : Seg := ⟨13247533154193127024751519153, 13247615924161154082554902193, 718178009, 1048576, [43834, 43839, 43844, 43850, 43855, 43860, 43866, 43871, 43876, 43882, 43887, 43893, 43898, 43903, 43909, 43914, 43919, 43925, 43930, 43935, 43941, 43946, 43951, 39048], 13286178263109292360299898977, 13286261263412467341251409307⟩
def ThetaRun21.s2 : Seg := ⟨13286178263109292360299898977, 13286261263412467341251409307, 720275161, 1048576, [43962, 43967, 43972, 43978, 43983, 43988, 43994, 43999, 44005, 44010, 44015, 44021, 44026, 44031, 44037, 44042, 44048, 44053, 44058, 44064, 44069, 44074, 44080, 36100], 13324935367255623050746699531, 13325018598030759598875640371⟩
def ThetaRun21.s3 : Seg := ⟨13324935367255623050746699531, 13325018598030759598875640371, 722372313, 1048576, [44090, 44095, 44100, 44106, 44111, 44117, 44122, 44127, 44133, 44138, 44143, 44149, 44154, 44160, 44165, 44170, 44176, 44181, 44187, 44192, 44197, 44203, 44208, 33152], 13363680680335809240878867766, 13363764141080069360119347782⟩
def ThetaRun21.s4 : Seg := ⟨13363680680335809240878867766, 13363764141080069360119347782, 724469465, 1048576, [44218, 44223, 44228, 44234, 44239, 44245, 44250, 44255, 44261, 44266, 44272, 44277, 44282, 44288, 44293, 44299, 44304, 44309, 44315, 44320, 44326, 44331, 44337, 30204], 13402334016163457587898581615, 13402417706033537593573548714⟩
def ThetaRun21.s5 : Seg := ⟨13402334016163457587898581615, 13402417706033537593573548714, 726566617, 1048576, [44346, 44351, 44356, 44362, 44367, 44373, 44378, 44384, 44389, 44394, 44400, 44405, 44411, 44416, 44421, 44427, 44432, 44438, 44443, 44449, 44454, 44459, 44465, 27256], 13441011263506044913805298875, 13441095182412432872144144338⟩
def ThetaRun21.s6 : Seg := ⟨13441011263506044913805298875, 13441095182412432872144144338, 728663769, 1048576, [44474, 44479, 44484, 44490, 44495, 44501, 44506, 44512, 44517, 44522, 44528, 44533, 44539, 44544, 44550, 44555, 44561, 44566, 44571, 44577, 44582, 44588, 44593, 24309], 13479550534381201473880770186, 13479634681361329311108465548⟩
def ThetaRun21.s7 : Seg := ⟨13479550534381201473880770186, 13479634681361329311108465548, 730760921, 1048576, [44602, 44607, 44612, 44618, 44623, 44629, 44634, 44640, 44645, 44651, 44656, 44662, 44667, 44672, 44678, 44683, 44689, 44694, 44700, 44705, 44711, 44716, 44722, 21360], 13518240553642474743043744688, 13518324929560302242999122455⟩
def ThetaRun21.s8 : Seg := ⟨13518240553642474743043744688, 13518324929560302242999122455, 732858073, 1048576, [44730, 44735, 44741, 44746, 44751, 44757, 44762, 44768, 44773, 44779, 44784, 44790, 44795, 44801, 44806, 44812, 44817, 44823, 44828, 44833, 44839, 44844, 44850, 18412], 13556923950170569737256366911, 13557008554970402236587025202⟩
def ThetaRun21.s9 : Seg := ⟨13556923950170569737256366911, 13557008554970402236587025202, 734955225, 1048576, [44858, 44863, 44869, 44874, 44880, 44885, 44890, 44896, 44901, 44907, 44912, 44918, 44923, 44929, 44934, 44940, 44945, 44951, 44956, 44962, 44967, 44973, 44978, 15465], 13595591664295815060286007490, 13595676498085894385285528212⟩
def ThetaRun21.s10 : Seg := ⟨13595591664295815060286007490, 13595676498085894385285528212, 737052377, 1048576, [44986, 44991, 44997, 45002, 45008, 45013, 45019, 45024, 45030, 45035, 45041, 45046, 45052, 45057, 45063, 45068, 45074, 45079, 45085, 45090, 45096, 45101, 45107, 12512], 13634277950409385586578341475, 13634363013471434922418623746⟩
def ThetaRun21.s11 : Seg := ⟨13634277950409385586578341475, 13634363013471434922418623746, 739149529, 1048576, [45114, 45119, 45125, 45130, 45136, 45141, 45147, 45152, 45158, 45163, 45169, 45174, 45180, 45185, 45191, 45196, 45202, 45207, 45213, 45218, 45224, 45229, 45235, 9568], 13673063041056505571475401802, 13673148334198711160531729516⟩
def ThetaRun21.s12 : Seg := ⟨13673063041056505571475401802, 13673148334198711160531729516, 741246681, 1048576, [45242, 45247, 45253, 45258, 45264, 45269, 45275, 45280, 45286, 45291, 45297, 45302, 45308, 45313, 45319, 45325, 45330, 45336, 45341, 45347, 45352, 45358, 45363, 6620], 13711757043536819805955698461, 13711842566690584210823370601⟩
def ThetaRun21.s13 : Seg := ⟨13711757043536819805955698461, 13711842566690584210823370601, 743343833, 1048576, [45370, 45375, 45381, 45386, 45392, 45397, 45403, 45408, 45414, 45419, 45425, 45431, 45436, 45442, 45447, 45453, 45458, 45464, 45469, 45475, 45481, 45486, 45492, 3672], 13750407032798595059403596116, 13750492786072213694009847038⟩
def ThetaRun21.s14 : Seg := ⟨13750407032798595059403596116, 13750492786072213694009847038, 745440985, 1048576, [45498, 45503, 45509, 45514, 45520, 45525, 45531, 45536, 45542, 45548, 45553, 45559, 45564, 45570, 45575, 45581, 45587, 45592, 45598, 45603, 45609, 45614, 45620, 725], 13788982444842823808030560863, 13789068428434251235248176514⟩
def ThetaRun21.s15 : Seg := ⟨13788982444842823808030560863, 13789068428434251235248176514, 747538137, 1048576, [45626, 45631, 45637, 45642, 45648, 45653, 45659, 45665, 45670, 45676, 45681, 45687, 45692, 45698, 45704, 45709, 45715, 45720, 45726, 45732, 45737, 45743, 43525], 13827618937314685839913853385, 13827705151234416577679879541⟩
def ThetaRun21.s16 : Seg := ⟨13827618937314685839913853385, 13827705151234416577679879541, 749635289, 1048576, [45754, 45759, 45765, 45770, 45776, 45782, 45787, 45793, 45798, 45804, 45809, 45815, 45821, 45826, 45832, 45837, 45843, 45849, 45854, 45860, 45865, 45871, 40706], 13866283717169611721923456303, 13866370160999251705813011770⟩

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