New Syracuse step-14 certificate classes, chunk 5
DefinitionsyracuseSevenMod32New26Step14Chunk05Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 5 of 5 of the newly certifiable residue classes modulo with accelerated Syracuse descent time and total stripped exponent . This chunk contains 677 exact residue representatives and is kept moderate in size for reusable Lean compilation.
Definition code
import Mathlib.Data.Finset.Insert
set_option maxRecDepth 200000
def syracuseSevenMod32New26Step14Chunk05Classes : Finset ℕ := {
54151527, 54167143, 54168391, 54172391, 54179687, 54225735, 54229735, 54231783, 54260967,
54289127, 54296647, 54353767, 54356039, 54375655, 54402215, 54403815, 54411111, 54428775,
54505383, 54522599, 54528871, 54540615, 54597959, 54600007, 54625767, 54629191, 54629991,
54657351, 54658151, 54667495, 54672743, 54700903, 54730087, 54743879, 54749351, 54751975,
54772039, 54789479, 54808743, 54810343, 54844775, 54866087, 54873959, 54890823, 54932327,
54966183, 54993991, 55004263, 55007335, 55035719, 55038119, 55040167, 55049063, 55063655,
55066727, 55077223, 55101159, 55120199, 55123047, 55124071, 55157479, 55160551, 55178567,
55217895, 55259047, 55279463, 55310695, 55316967, 55385255, 55443623, 55448295, 55469383,
55470183, 55488423, 55511911, 55525703, 55527527, 55528775, 55568231, 55586119, 55598439,
55621351, 55685191, 55719847, 55736039, 55765671, 55799655, 55816519, 55823015, 55839207,
55846503, 55882983, 55889255, 55896999, 55909095, 55940327, 55948647, 55954343, 55968487,
55989575, 55990375, 55997095, 56018535, 56023655, 56046695, 56048743, 56053415, 56070631,
56079975, 56090471, 56104263, 56117479, 56142567, 56184743, 56205159, 56207431, 56251207,
56264551, 56277319, 56305127, 56308551, 56336711, 56362471, 56400551, 56405223, 56409447,
56418791, 56428711, 56437607, 56438855, 56485703, 56488103, 56510791, 56511591, 56527207,
56540775, 56583527, 56588199, 56611687, 56662759, 56671079, 56673351, 56683623, 56699239,
56717479, 56730695, 56773447, 56787015, 56807079, 56808679, 56872295, 56958823, 57005671,
57030983, 57031783, 57043175, 57099495, 57103719, 57126055, 57162087, 57176903, 57182375,
57183399, 57206887, 57239719, 57243367, 57247591, 57287143, 57300711, 57309031, 57346535,
57357479, 57378919, 57388263, 57411399, 57411751, 57422695, 57440359, 57467719, 57510247,
57531111, 57537383, 57590503, 57611591, 57655367, 57668935, 57714759, 57728103, 57740647,
57756487, 57760935, 57762535, 57765607, 57787495, 57797991, 57821927, 57844839, 57881319,
57884519, 57887591, 57899335, 57900135, 57901159, 57938663, 57958727, 57972071, 57988711,
58026215, 58031463, 58047079, 58059623, 58079911, 58106023, 58108071, 58130759, 58133831,
58169063, 58190151, 58190951, 58203495, 58249543, 58267559, 58306887, 58366055, 58378599,
58394439, 58422375, 58456807, 58459879, 58464103, 58488039, 58502055, 58522471, 58537287,
58543783, 58558375, 58600103, 58617767, 58666343, 58669415, 58675111, 58675687, 58711143,
58744423, 58748647, 58774183, 58783079, 58802343, 58825031, 58828103, 58838247, 58856263,
58857063, 58861735, 58870631, 58894567, 58926951, 59025895, 59043911, 59044711, 59078567,
59083239, 59091111, 59101031, 59102055, 59116871, 59147879, 59193255, 59205223, 59206471,
59241703, 59262791, 59269863, 59299047, 59332455, 59349095, 59377255, 59391847, 59394119,
59420007, 59429351, 59440295, 59441895, 59451463, 59471079, 59477351, 59485095, 59527847,
59563879, 59609927, 59623271, 59636839, 59638087, 59667271, 59679591, 59708775, 59710823,
59721191, 59738983, 59763943, 59777511, 59785383, 59797575, 59810119, 59839303, 59846823,
59848423, 59882855, 59927655, 59960487, 59970407, 60021479, 60026727, 60029799, 60078247,
60089415, 60101735, 60104807, 60132167, 60134567, 60136167, 60143463, 60145735, 60165799,
60167399, 60198631, 60216647, 60217447, 60348775, 60355047, 60389703, 60406119, 60433255,
60462439, 60486375, 60504391, 60508263, 60535623, 60537447, 60565607, 60566855, 60580199,
60602087, 60621927, 60645863, 60659431, 60700583, 60723271, 60737639, 60746983, 60757927,
60767847, 60770471, 60803751, 60827239, 60831463, 60837735, 60854599, 60888231, 60921063,
60935079, 60949223, 60970311, 61001895, 61006567, 61014087, 61027655, 61056615, 61069159,
61071207, 61086823, 61099367, 61108711, 61115207, 61124327, 61150439, 61166055, 61180647,
61199687, 61222823, 61258855, 61264551, 61280743, 61289287, 61317447, 61330791, 61343207,
61358951, 61374791, 61390183, 61399527, 61405799, 61438631, 61447527, 61464743, 61469415,
61476935, 61492551, 61518663, 61527783, 61534279, 61548871, 61572583, 61615335, 61626279,
61628903, 61643495, 61648967, 61649767, 61709159, 61711431, 61766503, 61767751, 61779047,
61822823, 61837639, 61860775, 61870247, 61896007, 61917095, 61940807, 61983559, 61997127,
62011719, 62017191, 62034407, 62043751, 62069863, 62081255, 62107367, 62128231, 62137575,
62161063, 62164135, 62187623, 62205863, 62220455, 62281447, 62325223, 62402631, 62403431,
62416999, 62441959, 62449479, 62460775, 62475591, 62505799, 62510823, 62569191, 62624935,
62632807, 62649671, 62663015, 62681255, 62685927, 62691175, 62693447, 62799015, 62807911,
62810183, 62825575, 62827175, 62829799, 62843815, 62845415, 62855335, 62857959, 62879047,
62886567, 62919399, 62937415, 62938215, 62975719, 63010151, 63026791, 63038311, 63054151,
63064295, 63095655, 63126887, 63146151, 63198023, 63213639, 63226183, 63258215, 63287623,
63298919, 63300967, 63305639, 63329127, 63343943, 63404135, 63432519, 63442791, 63458407,
63460455, 63497959, 63524519, 63552231, 63606951, 63608999, 63655847, 63712167, 63764839,
63791975, 63821159, 63845095, 63849319, 63866183, 63896167, 63920455, 63935847, 63938919,
63957735, 64023399, 64059303, 64063975, 64082791, 64116647, 64126567, 64129191, 64185959,
64187559, 64190183, 64213319, 64215719, 64246951, 64248551, 64279783, 64288679, 64293351,
64312167, 64325959, 64342375, 64360615, 64370535, 64387175, 64420583, 64432199, 64467431,
64558407, 64581543, 64616775, 64618599, 64630119, 64639463, 64648007, 64659303, 64661575,
64701927, 64711399, 64717671, 64737959, 64758247, 64759271, 64764519, 64788807, 64802023,
64815591, 64820839, 64825511, 64828135, 64835655, 64848999, 64858343, 64908391, 64914663,
64969383, 64984999, 64997543, 65002215, 65007687, 65070151, 65079623, 65125223, 65126471,
65127495, 65137767, 65170247, 65181543, 65183815, 65196359, 65203879, 65205479, 65226567,
65228967, 65231591, 65261223, 65282887, 65296231, 65317543, 65341031, 65345703, 65370439,
65383783, 65386855, 65443175, 65486951, 65500519, 65518183, 65528679, 65546343, 65564583,
65573703, 65576103, 65599815, 65616231, 65640167, 65643367, 65668327, 65696487, 65702759,
65738663, 65747559, 65785063, 65808551, 65968039, 65987303, 65990503, 65991527, 66008391,
66021735, 66036551, 66044647, 66064711, 66098343, 66146791, 66153287, 66162407, 66181223,
66185895, 66188519, 66209383, 66216679, 66237543, 66245287, 66275047, 66318823, 66329767,
66338663, 66355527, 66368871, 66397031, 66412871, 66428263, 66432935, 66443879, 66485607,
66515015, 66530631, 66556743, 66565863, 66584903, 66616935, 66643271, 66657639, 66659687,
66677927, 66687047, 66701415, 66734247, 66747239, 66803559, 66860903, 66884839, 66898855,
66908327, 66934087, 66955175, 66967719, 66976615, 66991207, 67004775, 67020391, 67028711,
67056871, 67063143
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.