New Syracuse step-15 certificate classes, chunk 3
DefinitionsyracuseSevenMod32New26Step15Chunk03Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 3 of 13 of the newly certifiable residue classes modulo with accelerated Syracuse descent time and total stripped exponent . This chunk contains 746 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 syracuseSevenMod32New26Step15Chunk03Classes : Finset ℕ := {
10803559, 10806599, 10829671, 10834759, 10846535, 10847559, 10850375, 10869415, 10888039,
10897223, 10900647, 10903879, 10910567, 10919271, 10920295, 10923111, 10945383, 10947431,
10963047, 10966887, 10976615, 10979655, 10980455, 10981703, 10993831, 11004775, 11021639,
11028551, 11054439, 11056871, 11063783, 11071655, 11075911, 11076711, 11084871, 11095143,
11119463, 11121127, 11131047, 11133671, 11148647, 11154535, 11155367, 11162279, 11191015,
11192039, 11192423, 11201767, 11213927, 11220199, 11225255, 11226471, 11238247, 11251431,
11258535, 11282023, 11284647, 11292519, 11293159, 11304103, 11307751, 11323751, 11341159,
11343015, 11349927, 11365095, 11373415, 11375847, 11385959, 11389863, 11391655, 11401575,
11401959, 11402407, 11404007, 11407847, 11425095, 11425895, 11430759, 11432007, 11454055,
11456679, 11467623, 11479783, 11486055, 11487079, 11489351, 11500647, 11501895, 11511399,
11525991, 11542631, 11554151, 11559239, 11560263, 11561063, 11563495, 11565735, 11569991,
11574631, 11585383, 11586023, 11588423, 11601767, 11604839, 11611495, 11619655, 11623079,
11631783, 11631975, 11649191, 11660135, 11661383, 11668839, 11675975, 11698023, 11709607,
11713639, 11733095, 11733319, 11737767, 11742439, 11744071, 11749735, 11768999, 11770183,
11772231, 11776071, 11797991, 11800231, 11802215, 11814759, 11825319, 11826919, 11828327,
11829991, 11833191, 11839719, 11844967, 11848007, 11848807, 11851879, 11854311, 11857575,
11873127, 11892583, 11893607, 11896039, 11913703, 11919527, 11921767, 11924199, 11930087,
11931719, 11946087, 11949927, 11951975, 11954247, 11963495, 11965543, 11971047, 11973863,
11976295, 11979111, 11983207, 11987815, 11987879, 11989479, 11997351, 12002023, 12027367,
12040359, 12044199, 12063847, 12067687, 12070119, 12087975, 12098279, 12110663, 12138407,
12152999, 12157671, 12161511, 12163943, 12166215, 12170855, 12195143, 12198215, 12203239,
12207943, 12208359, 12222535, 12228199, 12229799, 12233447, 12233831, 12241575, 12264263,
12264679, 12265063, 12265703, 12270951, 12279655, 12281927, 12288167, 12292423, 12293223,
12298311, 12306791, 12307815, 12322023, 12330343, 12339271, 12342087, 12345511, 12350183,
12355431, 12357703, 12365159, 12370247, 12371047, 12374503, 12387047, 12387687, 12395591,
12396007, 12402279, 12412775, 12437095, 12438343, 12442983, 12444007, 12457575, 12466503,
12467303, 12472999, 12489191, 12491431, 12495079, 12509031, 12519591, 12522663, 12524647,
12525895, 12529735, 12539239, 12542311, 12551399, 12562151, 12569063, 12571463, 12576583,
12580583, 12598631, 12601671, 12602471, 12618919, 12624743, 12625831, 12626407, 12632903,
12633927, 12642407, 12659815, 12660647, 12673191, 12675239, 12682087, 12684135, 12690247,
12701543, 12718407, 12733799, 12736231, 12742727, 12743143, 12752039, 12755271, 12758887,
12761959, 12764231, 12771687, 12774503, 12781031, 12785255, 12790119, 12813031, 12814439,
12822759, 12823783, 12828007, 12831847, 12857415, 12858215, 12863303, 12871783, 12891239,
12893287, 12897959, 12904807, 12908903, 12919623, 12926119, 12930375, 12935015, 12937287,
12945767, 12948807, 12961959, 12965223, 12971879, 12972519, 12982439, 12983463, 12987495,
12993383, 12994631, 13020519, 13029223, 13029863, 13040231, 13065319, 13081319, 13086631,
13098151, 13102823, 13104455, 13110119, 13110951, 13111367, 13117799, 13128359, 13136039,
13142759, 13149255, 13159143, 13162599, 13165415, 13181255, 13190375, 13190759, 13190983,
13192007, 13233511, 13236583, 13249767, 13252967, 13253991, 13256423, 13260711, 13273255,
13280359, 13281127, 13282151, 13284583, 13293927, 13298599, 13312743, 13327975, 13334247,
13336679, 13339495, 13340743, 13341351, 13343591, 13348199, 13374183, 13378407, 13392999,
13398087, 13400743, 13417127, 13424231, 13428071, 13430503, 13437415, 13448359, 13449543,
13461735, 13471047, 13481575, 13504679, 13510983, 13519079, 13527367, 13531239, 13558599,
13563623, 13587559, 13588583, 13601959, 13617991, 13621415, 13624647, 13625063, 13625447,
13628263, 13641063, 13644903, 13652807, 13667175, 13680967, 13681383, 13682407, 13702471,
13731431, 13738727, 13742407, 13753703, 13759591, 13762663, 13766311, 13797479, 13798727,
13803367, 13805639, 13817959, 13829959, 13833383, 13839271, 13846119, 13851815, 13853415,
13860711, 13879207, 13887303, 13891943, 13895591, 13899623, 13903335, 13911783, 13912807,
13913191, 13931847, 13936551, 13949287, 13959655, 13972199, 13975399, 13976423, 13979303,
13993287, 13996519, 14024871, 14033767, 14035623, 14044519, 14049607, 14050631, 14053863,
14063783, 14066023, 14066407, 14091111, 14092135, 14099687, 14106951, 14110631, 14122343,
14123175, 14139559, 14145639, 14146663, 14150503, 14159207, 14166951, 14170791, 14179687,
14184167, 14198951, 14204007, 14216551, 14218599, 14221639, 14231015, 14246759, 14263399,
14265191, 14269287, 14271559, 14280007, 14281031, 14281831, 14294375, 14297831, 14306151,
14318695, 14323559, 14325607, 14327879, 14340423, 14352551, 14361447, 14362471, 14364743,
14381927, 14405287, 14422087, 14430375, 14434631, 14461607, 14467911, 14469479, 14470503,
14478183, 14485095, 14487719, 14488743, 14489767, 14507367, 14513255, 14514087, 14518759,
14520999, 14537575, 14547687, 14550759, 14551143, 14552391, 14555815, 14560487, 14572647,
14578343, 14578919, 14583975, 14596967, 14599239, 14610151, 14613351, 14625127, 14629991,
14640743, 14644583, 14644967, 14647655, 14649255, 14651879, 14654311, 14666055, 14672743,
14688359, 14699879, 14701735, 14708647, 14709223, 14723815, 14729063, 14732967, 14734567,
14748135, 14757223, 14760295, 14760679, 14761127, 14777511, 14784615, 14797159, 14812775,
14838503, 14841959, 14843751, 14844775, 14845799, 14859367, 14886375, 14886983, 14893223,
14912871, 14915911, 14918983, 14920615, 14922215, 14928711, 14929127, 14947143, 14947943,
14950567, 14952615, 14953191, 14960487, 14962343, 14978375, 14981799, 14985447, 14986471,
15009959, 15013191, 15020103, 15021287, 15027559, 15041767, 15051111, 15072359, 15077447,
15091815, 15092039, 15096487, 15102791, 15108455, 15114087, 15116359, 15116775, 15124647,
15128903, 15135591, 15156711, 15164775, 15166183, 15172455, 15187047, 15188711, 15206503,
15206727, 15211175, 15213031, 15215847, 15243431, 15252327, 15254599, 15263079, 15275623,
15280487, 15282919, 15284135, 15290439, 15297351, 15309671, 15313127, 15321415, 15332583,
15345511, 15346599, 15353671, 15354695, 15360743, 15363175, 15364967, 15387303, 15388327,
15389511, 15396007, 15409991, 15410791, 15416039, 15422567, 15424167, 15426407, 15438951,
15452327, 15456999, 15460071, 15472807, 15482727, 15484999, 15492455, 15501799, 15510887,
15516391, 15519591, 15520231, 15524935, 15531175, 15532775, 15534407, 15540071, 15543527,
15556935, 15576935, 15578983, 15581255, 15584071, 15586919, 15592551, 15618727, 15623783,
15624423, 15629671, 15634919, 15649895, 15651143, 15654759, 15655783, 15658663, 15680743,
15681351, 15700807, 15712103, 15714151, 15728967, 15760999, 15770471, 15784263, 15795815,
15801703, 15818919, 15821991, 15823591, 15825223, 15828295, 15829863, 15831719, 15838567,
15841639, 15845479, 15867751, 15870023, 15878311, 15881383, 15883367, 15884615, 15888455,
15897959, 15900999, 15901031, 15911751, 15916199, 15917415, 15920871, 15926759, 15938727,
15939303, 15957351, 15958375, 15972967, 15973735, 15977191, 15985511, 15992647, 16001127,
16003143, 16004967, 16019367, 16037799, 16048967, 16057447, 16071015, 16094951, 16099175,
16101863, 16117607, 16120679, 16123111, 16133223, 16139751, 16151271, 16157543
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.