New Syracuse step-15 certificate classes, chunk 10
DefinitionsyracuseSevenMod32New26Step15Chunk10Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 10 of 13 of the newly certifiable residue classes modulo with accelerated Syracuse descent time and total stripped exponent . This chunk contains 745 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 syracuseSevenMod32New26Step15Chunk10Classes : Finset ℕ := {
47090791, 47092839, 47095655, 47096679, 47097927, 47106407, 47125863, 47127911, 47132583,
47138279, 47156071, 47158503, 47168615, 47172519, 47181031, 47186663, 47194599, 47195207,
47202471, 47207751, 47214663, 47222119, 47225159, 47227207, 47256391, 47263911, 47264487,
47265511, 47299943, 47308647, 47322439, 47327079, 47328103, 47343719, 47344743, 47345575,
47355495, 47365991, 47371079, 47377575, 47380807, 47381607, 47387495, 47392999, 47397223,
47402311, 47414887, 47423335, 47425607, 47431271, 47437543, 47438567, 47443815, 47446887,
47449319, 47472231, 47472807, 47475431, 47475879, 47477479, 47495335, 47499367, 47506503,
47508711, 47514983, 47518823, 47521895, 47525095, 47526727, 47528551, 47532199, 47541095,
47549255, 47551655, 47553255, 47554887, 47558503, 47559527, 47560551, 47562823, 47566055,
47571303, 47574119, 47582887, 47584487, 47584871, 47589543, 47615719, 47622375, 47627623,
47631463, 47632711, 47633735, 47634535, 47636967, 47639207, 47658855, 47667943, 47671399,
47696359, 47705255, 47733415, 47749031, 47753703, 47756519, 47761223, 47765863, 47770535,
47772135, 47772519, 47777383, 47787111, 47805767, 47806791, 47817543, 47818343, 47822183,
47823207, 47828839, 47843655, 47845703, 47850343, 47860071, 47875687, 47876935, 47879527,
47880935, 47888231, 47893319, 47897191, 47901799, 47903463, 47921479, 47925351, 47934279,
47938279, 47940327, 47952711, 47953511, 47954535, 47969511, 47982695, 47983943, 47990599,
47991015, 47994215, 47997287, 47997671, 48000935, 48005191, 48019175, 48022375, 48032103,
48036167, 48039015, 48052583, 48062311, 48062951, 48064583, 48076519, 48079719, 48084199,
48110759, 48112359, 48117671, 48119655, 48121927, 48124743, 48137319, 48140359, 48147815,
48154727, 48157159, 48164071, 48175015, 48183911, 48184935, 48187559, 48213927, 48220839,
48221415, 48231143, 48237415, 48244327, 48244903, 48248551, 48249159, 48254823, 48255655,
48271687, 48305319, 48306503, 48308551, 48334311, 48337735, 48338151, 48338535, 48352167,
48359239, 48361639, 48363239, 48365895, 48366311, 48366695, 48376039, 48380263, 48381287,
48385127, 48387399, 48404391, 48409447, 48418983, 48423655, 48426855, 48427879, 48431175,
48438631, 48444743, 48452423, 48457895, 48460519, 48466791, 48473703, 48478951, 48480583,
48486247, 48488295, 48498023, 48503911, 48516455, 48517287, 48518887, 48525383, 48525799,
48532295, 48533671, 48541415, 48553319, 48567527, 48574631, 48582503, 48583143, 48589639,
48597735, 48599367, 48616775, 48624871, 48639911, 48640871, 48653031, 48674727, 48675943,
48681639, 48697831, 48702535, 48706375, 48712807, 48715879, 48731463, 48734535, 48744263,
48746663, 48747879, 48748711, 48755559, 48757607, 48760295, 48772199, 48775015, 48775271,
48776039, 48785767, 48791655, 48791879, 48807271, 48809703, 48816615, 48822887, 48828743,
48831591, 48832615, 48847175, 48847975, 48855719, 48864615, 48866023, 48869095, 48881831,
48885479, 48886503, 48887111, 48893607, 48894023, 48909639, 48922983, 48926439, 48935751,
48944871, 48945255, 48951367, 48965959, 48967591, 48980711, 48988007, 48989671, 48993095,
48999591, 49019239, 49021255, 49025511, 49032423, 49043367, 49045991, 49055911, 49060583,
49066055, 49066855, 49076583, 49093799, 49093991, 49102695, 49116903, 49126247, 49128519,
49137767, 49152167, 49156839, 49161063, 49170599, 49177927, 49178727, 49182567, 49183591,
49184839, 49196135, 49196967, 49215399, 49218407, 49220071, 49220455, 49234247, 49236071,
49237319, 49238887, 49239911, 49253703, 49254727, 49276775, 49277863, 49287335, 49294663,
49306983, 49313095, 49313895, 49326439, 49329895, 49334183, 49348935, 49354599, 49357895,
49392487, 49393735, 49400647, 49412967, 49414215, 49421671, 49428391, 49428807, 49434279,
49441127, 49444583, 49451495, 49456743, 49460839, 49474215, 49485127, 49486951, 49490599,
49498343, 49508199, 49524455, 49525063, 49531559, 49545319, 49547751, 49554663, 49555047,
49578151, 49581223, 49581799, 49588295, 49591527, 49597799, 49604711, 49605543, 49616039,
49617639, 49621927, 49622951, 49637543, 49648871, 49657191, 49661031, 49662887, 49673575,
49674983, 49677031, 49698119, 49698535, 49698919, 49705639, 49727079, 49732199, 49740647,
49742311, 49754855, 49755239, 49757287, 49761959, 49779175, 49788519, 49799015, 49812807,
49819719, 49820519, 49826023, 49827175, 49834087, 49836519, 49851111, 49859047, 49864871,
49866567, 49877863, 49884519, 49892679, 49893287, 49913703, 49915975, 49922887, 49927911,
49950023, 49959751, 49971047, 49972711, 49973095, 49985255, 49985863, 49986279, 49986663,
50013671, 50017095, 50042023, 50043207, 50045255, 50049895, 50064487, 50066759, 50071015,
50080103, 50083751, 50098343, 50103015, 50108263, 50109095, 50110535, 50113767, 50117991,
50123079, 50127335, 50137255, 50146151, 50147399, 50158311, 50164583, 50179175, 50194247,
50196647, 50204743, 50216103, 50219335, 50220135, 50224999, 50227271, 50235751, 50242663,
50244263, 50246887, 50249319, 50260903, 50262503, 50272423, 50275047, 50292071, 50296135,
50296743, 50303655, 50304231, 50318247, 50320231, 50332391, 50336487, 50340935, 50343143,
50353479, 50354503, 50355303, 50367847, 50371303, 50379623, 50381895, 50382439, 50392167,
50392807, 50407783, 50411431, 50426023, 50427239, 50436967, 50439239, 50443879, 50454375,
50455399, 50471239, 50481383, 50481991, 50491303, 50495559, 50511719, 50512743, 50515623,
50517223, 50526535, 50527335, 50542951, 50543975, 50563239, 50580839, 50615111, 50617959,
50621159, 50630727, 50643271, 50660071, 50667367, 50672455, 50674279, 50675303, 50686823,
50700615, 50704711, 50711367, 50711783, 50714215, 50716007, 50718055, 50722727, 50735271,
50739527, 50740327, 50746215, 50751719, 50761031, 50762215, 50773351, 50782055, 50782695,
50801511, 50808039, 50812263, 50817127, 50821223, 50834599, 50849607, 50850983, 50859879,
50870631, 50875495, 50877543, 50879143, 50885447, 50890919, 50891943, 50894759, 50897767,
50904679, 50915047, 50915431, 50918247, 50941607, 50948263, 50951911, 50956135, 50969319,
50989383, 50995687, 51005799, 51009255, 51017575, 51021415, 51024039, 51026087, 51026663,
51028295, 51033959, 51055079, 51066023, 51072935, 51080007, 51084007, 51087463, 51096807,
51101031, 51115239, 51119943, 51120295, 51129255, 51130439, 51131239, 51143399, 51148903,
51150919, 51176263, 51181927, 51209063, 51218791, 51229927, 51238247, 51239655, 51244903,
51245927, 51258087, 51262183, 51265383, 51266407, 51283271, 51299047, 51313255, 51320135,
51337543, 51352935, 51354343, 51356007, 51363911, 51374823, 51377479, 51390823, 51394887,
51423303, 51436647, 51440487, 51449191, 51452231, 51465031, 51467623, 51469479, 51471079,
51474151, 51476391, 51481063, 51483463, 51484263, 51496039, 51499879, 51506535, 51511623,
51512423, 51521767, 51530471, 51533735, 51543655, 51546279, 51553383, 51584359, 51589863,
51593063, 51596135, 51598151, 51603047, 51603623, 51604647, 51606247, 51607271, 51607879,
51608679, 51609703, 51614375, 51626311, 51630407, 51632807, 51643751, 51647207, 51664039,
51664615, 51665639, 51666023, 51667271, 51680615, 51696871, 51697255, 51699047, 51703527,
51705767, 51710439, 51720359, 51722567, 51728231, 51729255, 51734759, 51740007, 51742823,
51743047, 51755623, 51759463, 51768167, 51777703, 51786599, 51787623, 51788455, 51804263,
51814567, 51816615, 51820455, 51837671, 51839303, 51842375, 51849287, 51858535, 51877607,
51884519, 51889991, 51892391, 51898695, 51899495, 51903335, 51912039, 51931495, 51958087,
51974471, 51975495, 51976103, 51978343, 51998631, 52015431, 52032839
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.