New Syracuse step-15 certificate classes, chunk 13
DefinitionsyracuseSevenMod32New26Step15Chunk13Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 13 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 syracuseSevenMod32New26Step15Chunk13Classes : Finset ℕ := {
62023271, 62025895, 62035815, 62036647, 62038087, 62039111, 62045543, 62050631, 62054887,
62064807, 62073703, 62075751, 62081863, 62083239, 62085863, 62089319, 62093991, 62096615,
62115495, 62116679, 62125799, 62137159, 62143207, 62143655, 62146887, 62150503, 62171815,
62176871, 62182759, 62183143, 62190055, 62195303, 62199975, 62202599, 62204231, 62204647,
62257767, 62267239, 62268487, 62269511, 62282055, 62298855, 62305127, 62314087, 62315687,
62321991, 62324583, 62328487, 62328903, 62339399, 62341223, 62351591, 62354791, 62376679,
62377063, 62382951, 62384807, 62408295, 62418855, 62423111, 62430375, 62431399, 62434471,
62454087, 62454119, 62457959, 62462631, 62464839, 62470503, 62473959, 62478247, 62491815,
62494023, 62497639, 62498663, 62502119, 62510439, 62511431, 62511463, 62515303, 62527655,
62538599, 62539239, 62551367, 62554215, 62558279, 62561127, 62567783, 62570823, 62572455,
62572871, 62585447, 62591719, 62601831, 62602855, 62610535, 62617447, 62634663, 62639335,
62642791, 62643367, 62643559, 62645607, 62648039, 62650279, 62662823, 62667079, 62673767,
62685543, 62704359, 62710631, 62719815, 62735591, 62739815, 62744679, 62744903, 62745703,
62758055, 62792935, 62805095, 62805927, 62816423, 62822311, 62826343, 62838951, 62842183,
62842599, 62844775, 62845799, 62870343, 62873191, 62875815, 62883687, 62898919, 62899943,
62907463, 62936807, 62952615, 62956263, 62959943, 62962343, 62977127, 62980199, 62993575,
63007559, 63015015, 63016263, 63036519, 63040167, 63042791, 63047847, 63049895, 63050919,
63058791, 63063655, 63070951, 63072583, 63074023, 63088999, 63091815, 63095911, 63103815,
63107239, 63108839, 63113127, 63117159, 63129319, 63130727, 63153255, 63157479, 63161159,
63165799, 63173095, 63177191, 63192935, 63193959, 63196007, 63210823, 63223143, 63224167,
63224551, 63240807, 63242407, 63245415, 63253159, 63267143, 63268167, 63271399, 63276647,
63283559, 63298151, 63304807, 63305031, 63307879, 63324487, 63328167, 63339879, 63357095,
63383655, 63384487, 63391335, 63397031, 63397223, 63411015, 63416487, 63419495, 63434087,
63436135, 63439175, 63440807, 63442247, 63443431, 63448551, 63454375, 63456999, 63458023,
63461287, 63471207, 63477063, 63497543, 63504871, 63511911, 63515367, 63525703, 63532199,
63537255, 63541319, 63543143, 63545415, 63555687, 63574759, 63588519, 63592775, 63593191,
63630055, 63639623, 63671399, 63674471, 63679143, 63684775, 63702631, 63705255, 63715175,
63716007, 63731623, 63738535, 63742119, 63744167, 63745191, 63755111, 63762599, 63768679,
63773351, 63786087, 63795879, 63796455, 63810471, 63811655, 63814503, 63816775, 63823015,
63824615, 63825223, 63826247, 63830887, 63852199, 63859047, 63862119, 63862503, 63870823,
63871847, 63873095, 63874663, 63883591, 63884007, 63888039, 63927143, 63928167, 63941351,
63942983, 63950503, 63952103, 63956327, 63960999, 63961415, 63963239, 63965671, 63975591,
63984487, 63995047, 63998279, 63999719, 64003943, 64005991, 64006823, 64034151, 64034983,
64052839, 64058471, 64095975, 64098791, 64100199, 64109159, 64110759, 64115815, 64124135,
64130407, 64141991, 64153319, 64160231, 64164679, 64170727, 64176999, 64178023, 64179879,
64189799, 64192839, 64193639, 64194471, 64199335, 64217959, 64230727, 64233575, 64236199,
64252231, 64259303, 64265575, 64274279, 64289895, 64292711, 64309575, 64311207, 64320327,
64322727, 64329639, 64333895, 64334311, 64367943, 64382311, 64383719, 64390631, 64391655,
64400551, 64403175, 64406631, 64419175, 64424039, 64428711, 64430567, 64438439, 64449383,
64456295, 64460967, 64464199, 64467015, 64484455, 64492359, 64498407, 64501671, 64505703,
64513639, 64517863, 64521543, 64524135, 64526183, 64528455, 64538951, 64563047, 64573607,
64583527, 64584551, 64586983, 64594279, 64612711, 64613543, 64620391, 64620455, 64621031,
64627527, 64637031, 64641703, 64643943, 64654439, 64656487, 64662183, 64674535, 64685671,
64688295, 64690343, 64702535, 64714663, 64722151, 64727207, 64733927, 64736167, 64737767,
64738151, 64750311, 64751719, 64751943, 64756391, 64757607, 64758855, 64759879, 64768359,
64771399, 64796519, 64798791, 64800359, 64810087, 64831591, 64836263, 64845159, 64851815,
64866631, 64872295, 64873319, 64886087, 64898279, 64903911, 64910183, 64932519, 64935143,
64955207, 64956007, 64961255, 64978535, 64984167, 64989255, 65029607, 65036455, 65039527,
65042759, 65049255, 65061991, 65063015, 65072359, 65076391, 65090375, 65095847, 65098919,
65102151, 65105991, 65107175, 65113447, 65118535, 65133735, 65134951, 65155239, 65156263,
65156839, 65174887, 65190503, 65191271, 65194727, 65200615, 65219431, 65222503, 65235047,
65236071, 65246823, 65248423, 65257319, 65259367, 65260007, 65266503, 65272135, 65272935,
65274983, 65284327, 65288551, 65303367, 65306215, 65312487, 65316711, 65319399, 65322599,
65329479, 65344871, 65350759, 65363559, 65364135, 65366375, 65367207, 65368807, 65381991,
65394535, 65397831, 65406311, 65410983, 65413223, 65413607, 65419879, 65421479, 65440583,
65444583, 65452711, 65462631, 65465447, 65471975, 65474215, 65475399, 65475815, 65484519,
65490791, 65502375, 65503975, 65525063, 65530535, 65550183, 65554023, 65559719, 65562951,
65568839, 65583015, 65595751, 65596583, 65619687, 65620711, 65625959, 65628231, 65640359,
65647847, 65652551, 65654951, 65657191, 65657575, 65663847, 65673383, 65678439, 65680711,
65685351, 65687623, 65700967, 65713511, 65714343, 65714535, 65735783, 65737031, 65737831,
65767015, 65770855, 65771687, 65779559, 65781831, 65788519, 65789095, 65792743, 65794791,
65795175, 65803495, 65812807, 65816679, 65840199, 65844039, 65850087, 65852743, 65856359,
65872199, 65874023, 65878695, 65881703, 65885543, 65888999, 65897959, 65909863, 65931175,
65943911, 65944935, 65947367, 65954279, 65954663, 65961575, 65972071, 65973095, 65987911,
65988935, 66002087, 66004327, 66010983, 66016071, 66018919, 66021543, 66022567, 66025799,
66028647, 66046055, 66050727, 66055847, 66078887, 66080935, 66082535, 66094311, 66098535,
66105255, 66108071, 66112167, 66116775, 66125671, 66128743, 66135655, 66160743, 66160967,
66163015, 66163815, 66169319, 66171719, 66173543, 66177767, 66185063, 66196647, 66204519,
66205543, 66216295, 66218311, 66221159, 66252967, 66257223, 66258023, 66258663, 66266183,
66276455, 66281959, 66292903, 66295527, 66299751, 66299815, 66314983, 66315591, 66316391,
66319207, 66322503, 66329959, 66338919, 66357159, 66365031, 66394023, 66395239, 66408615,
66409639, 66417127, 66422375, 66429671, 66432743, 66435751, 66450535, 66450759, 66462535,
66465959, 66467559, 66473831, 66474471, 66520295, 66525927, 66531239, 66537543, 66543783,
66544359, 66545991, 66551655, 66566055, 66572775, 66572967, 66579815, 66582887, 66583271,
66586535, 66589159, 66607207, 66626887, 66630119, 66637991, 66642279, 66648935, 66650183,
66651623, 66661095, 66663527, 66663751, 66666343, 66666599, 66671271, 66677095, 66682983,
66683207, 66684007, 66705255, 66715815, 66720487, 66723943, 66726759, 66742375, 66749671,
66755943, 66757351, 66775783, 66778215, 66782055, 66785351, 66786535, 66792807, 66797895,
66800967, 66802151, 66813095, 66816743, 66829927, 66830503, 66835783, 66836199, 66842695,
66858087, 66870631, 66880999, 66888519, 66890919, 66894151, 66900647, 66912583, 66914215,
66914407, 66919079, 66940999, 66951495, 66954343, 66956135, 66957383, 66958183, 66985319,
66988775, 66996071, 66998343, 67008231, 67017575, 67019847, 67029319, 67033767, 67037863,
67043495, 67063975, 67073895, 67074727, 67074919, 67088711, 67100839
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.