New Syracuse step-15 certificate classes, chunk 8
DefinitionsyracuseSevenMod32New26Step15Chunk08Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 8 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 syracuseSevenMod32New26Step15Chunk08Classes : Finset ℕ := {
36575143, 36587879, 36588903, 36598247, 36604743, 36610791, 36616039, 36626791, 36631879,
36636135, 36639975, 36648679, 36654951, 36666087, 36669543, 36678887, 36689223, 36690023,
36738279, 36747175, 36748391, 36752295, 36760743, 36760935, 36761767, 36787527, 36800871,
36803911, 36807783, 36808615, 36816711, 36819111, 36840167, 36842215, 36842599, 36844871,
36864103, 36865127, 36878503, 36896935, 36899943, 36901191, 36901607, 36901991, 36904807,
36905831, 36920423, 36933799, 36943719, 36957927, 36958951, 36962151, 36966471, 36967271,
36967655, 36979015, 36995431, 36997863, 37004359, 37008199, 37016903, 37034311, 37045479,
37045863, 37047111, 37051751, 37062119, 37066343, 37074023, 37088615, 37091687, 37094503,
37095527, 37100199, 37103847, 37104871, 37106503, 37111527, 37118439, 37128359, 37166247,
37168487, 37169895, 37176167, 37187751, 37188327, 37189351, 37191783, 37198695, 37208391,
37210439, 37216743, 37225831, 37235559, 37245095, 37255847, 37269415, 37269831, 37279335,
37281127, 37291879, 37292519, 37292903, 37303463, 37305063, 37310311, 37316839, 37326151,
37327175, 37335879, 37338727, 37342567, 37349223, 37366087, 37380455, 37386343, 37398887,
37399719, 37402535, 37413703, 37422183, 37423207, 37427047, 37427879, 37430343, 37446119,
37457063, 37463975, 37472071, 37473095, 37474471, 37479751, 37480551, 37486663, 37502055,
37503079, 37513575, 37523303, 37538119, 37541735, 37556551, 37557575, 37559399, 37563047,
37565671, 37571943, 37582695, 37584967, 37596903, 37637991, 37638055, 37658471, 37660743,
37673287, 37685063, 37686631, 37687463, 37690087, 37694375, 37695399, 37706919, 37731431,
37734311, 37746023, 37754727, 37764711, 37767911, 37771367, 37802151, 37814343, 37821607,
37827303, 37827687, 37846119, 37851623, 37858535, 37889895, 37890727, 37890919, 37901671,
37906535, 37921511, 37924775, 37933895, 37948263, 37954791, 37965127, 37978279, 37980519,
37980903, 37994087, 38000359, 38001767, 38004583, 38025895, 38036839, 38037671, 38039271,
38041511, 38046183, 38054055, 38058311, 38061159, 38064999, 38073703, 38086119, 38087911,
38098663, 38118503, 38121319, 38122343, 38136135, 38136935, 38152935, 38161255, 38168167,
38194279, 38195527, 38202023, 38207655, 38217575, 38219847, 38220647, 38226759, 38236007,
38237031, 38238887, 38261991, 38264999, 38274919, 38277991, 38289735, 38319335, 38323015,
38327655, 38328039, 38333351, 38340199, 38345447, 38349127, 38362471, 38368359, 38368583,
38376103, 38384999, 38402663, 38405863, 38406247, 38407495, 38410919, 38412135, 38414407,
38426727, 38427751, 38434023, 38440295, 38450023, 38452071, 38454343, 38454887, 38456135,
38458983, 38460007, 38460583, 38465255, 38466887, 38480231, 38483047, 38496487, 38498471,
38502759, 38504359, 38506343, 38516327, 38521159, 38521575, 38553831, 38557031, 38563751,
38579303, 38584167, 38585191, 38588071, 38599783, 38615399, 38615783, 38616231, 38623143,
38630215, 38639719, 38641511, 38643559, 38653287, 38667879, 38672551, 38684135, 38687559,
38693607, 38696263, 38699111, 38713671, 38717351, 38736615, 38740455, 38748327, 38759271,
38767975, 38774087, 38775719, 38779559, 38782567, 38784231, 38788263, 38802247, 38807719,
38812775, 38830439, 38833479, 38834663, 38849255, 38855527, 38864711, 38873959, 38889799,
38890599, 38906215, 38922055, 38923431, 38924455, 38926055, 38927463, 38937831, 38947943,
38951591, 38961319, 38971239, 38977127, 38984007, 38984423, 38990695, 39018087, 39028583,
39041767, 39047015, 39052359, 39061831, 39075431, 39078247, 39096487, 39098535, 39104839,
39106407, 39107239, 39108679, 39118183, 39122023, 39125095, 39152455, 39153831, 39169255,
39181415, 39187687, 39192743, 39201703, 39202887, 39215847, 39217479, 39218919, 39233895,
39251111, 39258023, 39262055, 39277671, 39281511, 39291239, 39294279, 39306055, 39308647,
39315175, 39322087, 39337831, 39340903, 39347559, 39352647, 39354471, 39356903, 39369063,
39369447, 39371495, 39386279, 39398055, 39409991, 39410791, 39421543, 39434087, 39448295,
39449703, 39463271, 39468135, 39473063, 39478887, 39481511, 39485799, 39500391, 39528551,
39537479, 39540071, 39555911, 39556711, 39562407, 39568231, 39569255, 39581031, 39584071,
39584871, 39585703, 39587143, 39594215, 39599271, 39618727, 39622375, 39638375, 39656807,
39658215, 39678695, 39679719, 39683399, 39683943, 39688039, 39690311, 39700583, 39713383,
39716199, 39720871, 39722855, 39725127, 39733415, 39736487, 39737671, 39739719, 39745383,
39756135, 39769703, 39771303, 39778215, 39780199, 39782887, 39794407, 39800679, 39801703,
39807207, 39812455, 39815271, 39816295, 39816519, 39819367, 39824039, 39824615, 39829671,
39832295, 39840615, 39847527, 39848103, 39876519, 39876711, 39887015, 39889255, 39892903,
39900007, 39912551, 39917415, 39933863, 39946599, 39954279, 39955367, 39956967, 39962439,
39964839, 39969511, 39975783, 39990599, 39994855, 40007015, 40019559, 40024231, 40026439,
40028263, 40037607, 40046919, 40047719, 40047943, 40053415, 40061095, 40079527, 40090279,
40096999, 40099175, 40101223, 40105895, 40113383, 40120487, 40128359, 40129383, 40139943,
40142951, 40144615, 40151111, 40159591, 40162631, 40175431, 40184743, 40192839, 40200519,
40200935, 40201319, 40223847, 40234343, 40236391, 40260711, 40266599, 40275303, 40292519,
40298215, 40311975, 40317671, 40322919, 40325191, 40337511, 40337735, 40347239, 40363079,
40378471, 40405831, 40410471, 40415143, 40425063, 40427687, 40432743, 40434791, 40435815,
40438631, 40458919, 40462567, 40465223, 40467623, 40481607, 40492135, 40494951, 40512839,
40526183, 40529639, 40535527, 40542375, 40548071, 40562023, 40568743, 40569159, 40575463,
40585575, 40591847, 40594279, 40627303, 40632807, 40638055, 40646567, 40650599, 40651623,
40666439, 40675559, 40679783, 40685895, 40693415, 40721127, 40727399, 40729447, 40731879,
40739175, 40741991, 40755367, 40757607, 40758439, 40760039, 40781927, 40801383, 40806887,
40812711, 40819431, 40823655, 40830791, 40835815, 40839271, 40863207, 40867047, 40872103,
40881063, 40895207, 40897863, 40900455, 40903751, 40913255, 40916295, 40917095, 40930663,
40941415, 40943687, 40960071, 40973415, 40998759, 41001031, 41017191, 41036455, 41043783,
41048807, 41054119, 41064039, 41069671, 41074535, 41077415, 41089351, 41090151, 41100103,
41100903, 41101543, 41105767, 41123431, 41126631, 41127015, 41128263, 41129063, 41130087,
41134759, 41142631, 41147495, 41157863, 41158247, 41175111, 41180775, 41181351, 41183975,
41184423, 41184999, 41186023, 41187655, 41200999, 41204039, 41207911, 41210343, 41217255,
41219431, 41223527, 41231431, 41235271, 41237095, 41240743, 41249639, 41252071, 41263431,
41266087, 41272935, 41274599, 41279847, 41280231, 41298087, 41306983, 41308839, 41317735,
41335399, 41336167, 41345511, 41360487, 41363303, 41367399, 41379943, 41384615, 41391719,
41397991, 41404903, 41413799, 41417031, 41419879, 41423719, 41429223, 41441959, 41450663,
41457383, 41457575, 41459559, 41469767, 41473767, 41481063, 41489767, 41494855, 41495655,
41496487, 41509031, 41517927, 41519975, 41526087, 41526887, 41527463, 41551207, 41552199,
41553223, 41554247, 41555879, 41564775, 41566375, 41568615, 41578567, 41584231, 41585479,
41589479, 41595751, 41596775, 41607527, 41616871, 41620295, 41621095, 41633639, 41635687,
41642823, 41644199, 41646823, 41648455, 41648871, 41658599, 41678055, 41690983, 41706215,
41707623, 41713735, 41721191, 41766215, 41770855, 41773127, 41785255, 41785447, 41792743,
41797447, 41797799, 41799015, 41799847, 41813607, 41819303, 41820903
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.