New Syracuse step-15 certificate classes, chunk 12
DefinitionsyracuseSevenMod32New26Step15Chunk12Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 12 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 syracuseSevenMod32New26Step15Chunk12Classes : Finset ℕ := {
56977255, 56979943, 56985191, 56988839, 56990439, 56996167, 56997735, 57000007, 57007463,
57009511, 57013351, 57013575, 57014183, 57016423, 57036711, 57037671, 57045159, 57052487,
57055911, 57084071, 57093031, 57105575, 57112679, 57141063, 57142631, 57144679, 57145063,
57149351, 57151335, 57151975, 57157095, 57166151, 57166567, 57166951, 57168999, 57206503,
57208679, 57209319, 57213415, 57221863, 57223911, 57233063, 57243975, 57245799, 57260391,
57260775, 57283303, 57315495, 57316519, 57316711, 57317543, 57338599, 57343847, 57348167,
57358663, 57364391, 57391719, 57393319, 57419879, 57420711, 57424551, 57440167, 57452711,
57453735, 57455719, 57463655, 57473383, 57476199, 57477223, 57481895, 57500519, 57513287,
57513703, 57520199, 57523047, 57525319, 57529703, 57534791, 57536999, 57553639, 57557863,
57571047, 57574727, 57577543, 57579367, 57580391, 57581639, 57590087, 57591911, 57592135,
57596583, 57601255, 57604711, 57612199, 57622119, 57624743, 57628999, 57629799, 57635687,
57636711, 57644391, 57647463, 57651527, 57659047, 57660647, 57662823, 57666279, 57667303,
57674215, 57684135, 57685735, 57692007, 57706823, 57715367, 57731943, 57743527, 57754855,
57767015, 57767847, 57772519, 57791335, 57804519, 57808743, 57825191, 57832679, 57835111,
57837735, 57838951, 57856167, 57860839, 57881927, 57888423, 57894503, 57896103, 57898343,
57898727, 57903015, 57905223, 57910887, 57921863, 57923431, 57924263, 57926503, 57939271,
57942119, 57944743, 57955495, 57957095, 57969479, 57982823, 57988327, 57997223, 57998439,
58001895, 58004711, 58012839, 58019751, 58020327, 58020711, 58028871, 58031271, 58034503,
58035527, 58042439, 58050919, 58053959, 58069159, 58079079, 58092263, 58095719, 58115175,
58118823, 58123079, 58127719, 58129127, 58135015, 58139111, 58140743, 58146983, 58157927,
58172743, 58175975, 58185063, 58200903, 58213223, 58214247, 58229063, 58260071, 58266951,
58271591, 58290087, 58295527, 58301799, 58319015, 58322087, 58323687, 58325319, 58327143,
58338663, 58345575, 58348007, 58350247, 58356551, 58367847, 58370119, 58372935, 58376359,
58383079, 58388551, 58403751, 58410471, 58416295, 58419943, 58423207, 58426215, 58426855,
58442471, 58446503, 58446695, 58460487, 58466791, 58467815, 58473063, 58476903, 58477287,
58480551, 58483175, 58497351, 58503239, 58505063, 58507335, 58510567, 58518631, 58524135,
58529383, 58534055, 58536679, 58540903, 58544199, 58557543, 58566887, 58616935, 58620775,
58623207, 58633319, 58641063, 58643687, 58656615, 58663751, 58664551, 58677095, 58677927,
58691911, 58692711, 58693543, 58706087, 58710759, 58716231, 58724519, 58735271, 58751303,
58757799, 58763431, 58778695, 58784935, 58788167, 58795079, 58810695, 58821991, 58833767,
58835015, 58836039, 58842279, 58845511, 58846311, 58851399, 58871463, 58878791, 58883431,
58888039, 58890087, 58892359, 58899047, 58903271, 58904903, 58912423, 58914023, 58924135,
58935111, 58937511, 58940135, 58946407, 58955367, 58956967, 58961639, 58967911, 58969767,
58981479, 58982503, 58983527, 58991431, 58992871, 58997095, 59004775, 59011911, 59014759,
59021031, 59023207, 59025255, 59026087, 59049575, 59052199, 59054247, 59060135, 59072103,
59072679, 59075751, 59077351, 59077735, 59078983, 59092327, 59095399, 59114855, 59115239,
59119527, 59122151, 59143399, 59151719, 59161255, 59171175, 59179495, 59180519, 59193063,
59195495, 59199335, 59209063, 59213735, 59226727, 59237223, 59254887, 59258727, 59271271,
59271495, 59273127, 59282247, 59284647, 59291559, 59293543, 59296231, 59305127, 59308359,
59315047, 59324775, 59329863, 59348711, 59351911, 59361095, 59363495, 59365095, 59366119,
59372391, 59376871, 59386983, 59389255, 59402983, 59405031, 59409255, 59411303, 59422887,
59444327, 59445575, 59446375, 59447207, 59456103, 59457703, 59475559, 59479207, 59480231,
59483463, 59487079, 59488103, 59490375, 59493607, 59503719, 59511623, 59512039, 59515047,
59517095, 59535527, 59540199, 59545447, 59547719, 59548743, 59561287, 59590247, 59597543,
59618407, 59639719, 59655911, 59660967, 59662183, 59663207, 59664455, 59676583, 59681447,
59684071, 59689127, 59695847, 59698087, 59699047, 59699687, 59700071, 59704935, 59709607,
59710631, 59712231, 59716935, 59719527, 59730279, 59733319, 59734343, 59737191, 59745095,
59753191, 59771207, 59773255, 59802855, 59806887, 59807079, 59813799, 59837287, 59855335,
59861831, 59864423, 59870951, 59877863, 59880263, 59881063, 59882087, 59889767, 59892583,
59893607, 59894439, 59897063, 59908423, 59917927, 59918567, 59924839, 59925223, 59946087,
59949927, 59953831, 59965767, 59966567, 59981159, 59983591, 59990503, 60001447, 60004071,
60024135, 60024935, 60027367, 60037287, 60038311, 60038503, 60047207, 60052295, 60064071,
60067911, 60077415, 60080455, 60095655, 60102567, 60105575, 60112487, 60117159, 60118183,
60121415, 60136807, 60141479, 60152423, 60153191, 60171079, 60174503, 60182375, 60194151,
60220263, 60223559, 60234471, 60239175, 60246087, 60265287, 60274407, 60278631, 60281319,
60286791, 60291815, 60293447, 60297063, 60312679, 60315751, 60325479, 60338663, 60346535,
60351815, 60357479, 60358727, 60366183, 60368231, 60372071, 60372295, 60375143, 60379815,
60386471, 60388071, 60395591, 60406503, 60409959, 60432487, 60442791, 60455783, 60461223,
60465895, 60501351, 60503783, 60510695, 60512103, 60521639, 60525287, 60569447, 60593383,
60602279, 60602695, 60607399, 60609191, 60616871, 60619111, 60642631, 60649543, 60660039,
60662887, 60663719, 60675431, 60676263, 60685159, 60697319, 60699751, 60703591, 60704615,
60706887, 60713319, 60728935, 60733607, 60737255, 60750439, 60752039, 60756295, 60757095,
60765415, 60771687, 60774727, 60783271, 60790119, 60809383, 60812007, 60819303, 60822375,
60822759, 60834119, 60835943, 60853991, 60872007, 60872423, 60878919, 60893511, 60906855,
60931175, 60950631, 60955303, 60961607, 60970919, 60980839, 60983463, 60994407, 61017767,
61021351, 61024999, 61028263, 61031271, 61041831, 61042855, 61044455, 61047911, 61050727,
61065319, 61065543, 61069991, 61071847, 61074087, 61075111, 61090663, 61097575, 61098151,
61105479, 61113575, 61123687, 61124519, 61131239, 61131431, 61133639, 61139687, 61142951,
61146983, 61147623, 61150055, 61154919, 61160167, 61163239, 61166439, 61167463, 61180231,
61183079, 61188583, 61190983, 61193831, 61194407, 61197671, 61200743, 61204327, 61214887,
61222215, 61224807, 61235559, 61240647, 61241447, 61244903, 61254823, 61257063, 61257447,
61261735, 61274855, 61276903, 61278311, 61282983, 61287655, 61301223, 61314215, 61332071,
61355943, 61357159, 61375207, 61378407, 61384295, 61393223, 61394023, 61397671, 61398887,
61412679, 61427879, 61437799, 61440071, 61472871, 61481799, 61482215, 61484391, 61493735,
61497191, 61499463, 61505703, 61507911, 61513575, 61514599, 61515847, 61528391, 61531463,
61534695, 61539559, 61542567, 61545191, 61556807, 61563047, 61572967, 61576423, 61590439,
61592039, 61592231, 61604583, 61613127, 61613543, 61619815, 61625671, 61633191, 61643079,
61645127, 61654631, 61655879, 61661543, 61669447, 61669863, 61670887, 61682407, 61682791,
61685863, 61690535, 61703271, 61713639, 61717863, 61726567, 61737127, 61740199, 61743431,
61748455, 61756775, 61768935, 61778663, 61796519, 61805415, 61816167, 61835623, 61836007,
61850439, 61861735, 61861959, 61877351, 61891943, 61892775, 61900263, 61900647, 61901287,
61902919, 61907783, 61913415, 61913831, 61916263, 61944647, 61947495, 61953767, 61960263,
61960679, 61969575, 61971175, 61972807, 61979495, 61981767, 61992039
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.