New Syracuse step-15 certificate classes, chunk 4
DefinitionsyracuseSevenMod32New26Step15Chunk04Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 4 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 syracuseSevenMod32New26Step15Chunk04Classes : Finset ℕ := {
16164455, 16169127, 16171751, 16173159, 16182503, 16191815, 16192615, 16193447, 16205991,
16213863, 16227047, 16235175, 16239847, 16256679, 16258279, 16263335, 16263527, 16273255,
16284391, 16289095, 16289511, 16294983, 16304487, 16307527, 16308327, 16309351, 16321895,
16336487, 16342183, 16345415, 16345831, 16346215, 16346855, 16361831, 16381671, 16402151,
16403175, 16411495, 16437415, 16439655, 16442087, 16446311, 16456871, 16463175, 16468839,
16470087, 16481383, 16483431, 16487079, 16491335, 16492135, 16507975, 16519495, 16524135,
16538727, 16539975, 16549095, 16550727, 16554151, 16560039, 16571559, 16576231, 16577639,
16595271, 16601575, 16603815, 16608071, 16612711, 16624103, 16626503, 16629927, 16632551,
16636007, 16639847, 16640871, 16643303, 16652615, 16657319, 16657735, 16661159, 16671079,
16671463, 16680423, 16689319, 16692967, 16700071, 16713639, 16714055, 16715079, 16730471,
16736743, 16737127, 16747687, 16749895, 16754535, 16770375, 16771175, 16771399, 16782951,
16784551, 16786791, 16791463, 16793447, 16810311, 16820455, 16824679, 16838311, 16851815,
16863399, 16866407, 16880999, 16883047, 16887719, 16890535, 16900263, 16902887, 16903911,
16904935, 16917319, 16944455, 16947303, 16951783, 16959847, 16969799, 16979111, 16980711,
16984167, 16992327, 17000775, 17003623, 17008103, 17011527, 17011943, 17020839, 17025959,
17027559, 17039687, 17040103, 17041127, 17048647, 17061191, 17069287, 17082279, 17083303,
17104967, 17112423, 17118311, 17121383, 17126055, 17139623, 17156199, 17160871, 17162087,
17183975, 17188679, 17189031, 17190247, 17192103, 17199591, 17202023, 17208935, 17209511,
17212135, 17214567, 17232999, 17246439, 17258343, 17271111, 17271527, 17271911, 17272135,
17273159, 17302759, 17304935, 17312679, 17320007, 17330919, 17345895, 17348935, 17349735,
17355239, 17368423, 17368999, 17376327, 17380167, 17383591, 17392487, 17395783, 17408327,
17409127, 17409351, 17412583, 17422503, 17425127, 17431399, 17437511, 17438311, 17443559,
17445991, 17453735, 17464423, 17475175, 17475815, 17481063, 17483495, 17490407, 17498279,
17505383, 17511655, 17517927, 17524839, 17529511, 17532135, 17542887, 17552199, 17567815,
17580359, 17584615, 17595559, 17600231, 17607143, 17614663, 17618663, 17622887, 17623911,
17639751, 17640359, 17641383, 17653095, 17656551, 17664871, 17670983, 17677415, 17682279,
17683111, 17696871, 17699143, 17701543, 17706215, 17722215, 17723463, 17734375, 17740647,
17764007, 17778535, 17780807, 17793351, 17800039, 17811783, 17812583, 17820327, 17843815,
17844039, 17847463, 17851719, 17852519, 17854311, 17858631, 17866087, 17877479, 17879879,
17883303, 17896295, 17900359, 17906407, 17909479, 17911111, 17914535, 17927271, 17937639,
17942887, 17946983, 17952839, 17963751, 17964199, 17968455, 17975367, 17986887, 17991143,
18001255, 18003303, 18003687, 18007975, 18010599, 18021543, 18024775, 18033895, 18041191,
18060455, 18067367, 18067943, 18074439, 18078311, 18090855, 18091687, 18102183, 18102599,
18108071, 18109095, 18116775, 18121447, 18140263, 18143335, 18149031, 18183015, 18185063,
18197607, 18204519, 18213223, 18228455, 18241383, 18243431, 18245703, 18250919, 18251943,
18256999, 18265319, 18274631, 18274663, 18277703, 18279335, 18280935, 18293479, 18305863,
18311335, 18311911, 18318183, 18319207, 18320231, 18322663, 18331975, 18336679, 18345191,
18350823, 18359143, 18359367, 18371911, 18372327, 18378823, 18379431, 18402119, 18421351,
18429671, 18433895, 18436167, 18458855, 18462311, 18472807, 18483367, 18486439, 18489671,
18494311, 18499815, 18519655, 18521255, 18524903, 18530151, 18542759, 18544359, 18557159,
18562407, 18566247, 18569319, 18569895, 18596679, 18598055, 18602151, 18613479, 18621799,
18625639, 18633543, 18636967, 18638183, 18639591, 18641639, 18645863, 18646887, 18647527,
18649159, 18659495, 18660071, 18661703, 18663143, 18665319, 18679143, 18680135, 18682983,
18690887, 18693735, 18704231, 18706919, 18713415, 18719047, 18734439, 18735463, 18740551,
18747047, 18748647, 18751655, 18769511, 18782887, 18791783, 18797895, 18798695, 18801127,
18804391, 18811047, 18814119, 18826855, 18827079, 18835559, 18860519, 18868039, 18868583,
18872039, 18878951, 18889895, 18892519, 18893127, 18893927, 18897575, 18912359, 18912583,
18917287, 18925383, 18925735, 18930023, 18950887, 18951271, 18977447, 18981703, 18984295,
19007815, 19009863, 19010279, 19013479, 19014503, 19015751, 19025255, 19028295, 19029095,
19031367, 19034599, 19043495, 19045095, 19061927, 19066599, 19067623, 19075143, 19102439,
19104103, 19104487, 19116871, 19122919, 19161447, 19169351, 19177639, 19180711, 19182695,
19184743, 19200359, 19204199, 19208871, 19226471, 19227111, 19228743, 19240263, 19244903,
19247175, 19248359, 19256679, 19260743, 19263975, 19268839, 19274919, 19276519, 19284839,
19285479, 19292327, 19296999, 19298023, 19303271, 19307367, 19319111, 19331687, 19356775,
19363687, 19378087, 19378503, 19380903, 19390823, 19391847, 19394279, 19396519, 19401191,
19401575, 19402823, 19413319, 19420007, 19434823, 19435847, 19451239, 19469479, 19470663,
19472711, 19481831, 19491143, 19491943, 19507559, 19541223, 19545447, 19551335, 19552167,
19559079, 19564711, 19573607, 19588839, 19595335, 19606631, 19610727, 19615399, 19616583,
19622055, 19624679, 19625703, 19632199, 19635047, 19637063, 19644743, 19653703, 19665223,
19666247, 19668071, 19680615, 19683047, 19689959, 19699879, 19704551, 19705575, 19717479,
19723367, 19728871, 19739815, 19746727, 19761895, 19762503, 19769415, 19781735, 19796135,
19803047, 19804071, 19805031, 19822695, 19826535, 19838887, 19840103, 19842151, 19850055,
19859367, 19876967, 19880039, 19882855, 19909447, 19912871, 19930279, 19933927, 19936359,
19957063, 19962535, 19967207, 19970407, 19973863, 19990695, 19992903, 19993927, 19997543,
20019879, 20026727, 20029799, 20030183, 20033447, 20048615, 20051271, 20054119, 20058183,
20072775, 20073799, 20089191, 20094823, 20097095, 20109031, 20129895, 20130119, 20130727,
20143271, 20150183, 20152167, 20160679, 20162727, 20173671, 20183399, 20187239, 20189671,
20191911, 20194791, 20196583, 20204263, 20228967, 20231015, 20245607, 20251111, 20257959,
20263655, 20267879, 20290407, 20302151, 20306599, 20316327, 20320999, 20335431, 20337831,
20339431, 20342087, 20345703, 20361127, 20370663, 20383591, 20396775, 20398407, 20416839,
20417639, 20440935, 20442023, 20462247, 20471143, 20477255, 20484775, 20490407, 20498343,
20542695, 20557895, 20558311, 20560743, 20563015, 20564807, 20567655, 20568231, 20569255,
20570855, 20572487, 20573287, 20591719, 20605159, 20608743, 20615015, 20615655, 20617063,
20619335, 20624999, 20629223, 20630247, 20631879, 20657383, 20661479, 20662503, 20663655,
20672359, 20673383, 20685543, 20689223, 20692839, 20696743, 20707655, 20711911, 20718823,
20724071, 20730343, 20738887, 20741287, 20742311, 20752231, 20753063, 20761959, 20764999,
20776551, 20779175, 20780391, 20781223, 20781799, 20799079, 20802279, 20804711, 20807527,
20812455, 20823143, 20828839, 20842215, 20849127, 20855399, 20856999, 20864103, 20867943,
20869799, 20870375, 20888231, 20901607, 20910919, 20919399, 20919463, 20921447, 20924263,
20926119, 20926535, 20936039, 20939079, 20939111, 20940711, 20943335, 20964199, 20971687,
20973383, 20976967, 20983879, 20985063, 20997447, 20998471, 21000103, 21011815, 21015271,
21020519, 21025607, 21029703, 21030727, 21051751, 21053767, 21057447, 21060263, 21075879,
21077863, 21080135, 21087047, 21093095, 21098567, 21099367, 21126503, 21129959
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.