New Syracuse step-15 certificate classes, chunk 11
DefinitionsyracuseSevenMod32New26Step15Chunk11Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 11 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 syracuseSevenMod32New26Step15Chunk11Classes : Finset ℕ := {
52033863, 52035687, 52047207, 52056551, 52065095, 52071751, 52072167, 52074599, 52076391,
52078663, 52087143, 52102983, 52119015, 52128487, 52130919, 52134759, 52155047, 52161895,
52165351, 52168423, 52171239, 52172647, 52175335, 52176359, 52181607, 52196583, 52205895,
52210599, 52219111, 52231015, 52232679, 52237927, 52239527, 52242599, 52245223, 52245831,
52252327, 52252743, 52265063, 52266087, 52266919, 52275431, 52302567, 52308647, 52325479,
52326311, 52331751, 52336807, 52342695, 52357863, 52366183, 52374887, 52377959, 52381799,
52383655, 52384231, 52386471, 52402087, 52414631, 52419303, 52419687, 52422503, 52424775,
52432231, 52439975, 52440391, 52452967, 52457191, 52475623, 52482727, 52487239, 52491623,
52496711, 52498919, 52510887, 52519783, 52533575, 52536647, 52539463, 52542311, 52543559,
52544583, 52546791, 52554855, 52564807, 52565607, 52570279, 52574119, 52579175, 52587335,
52590311, 52591719, 52598631, 52600903, 52603111, 52613447, 52615847, 52620967, 52622567,
52635495, 52643655, 52646055, 52648679, 52653927, 52670791, 52677287, 52678311, 52693479,
52699975, 52700775, 52713319, 52726087, 52734439, 52734631, 52751207, 52752455, 52753255,
52758119, 52762791, 52763367, 52787111, 52787527, 52791783, 52794599, 52799655, 52800871,
52803943, 52808615, 52809575, 52810599, 52822759, 52825415, 52828007, 52843847, 52844647,
52856423, 52860263, 52867143, 52872807, 52900967, 52901799, 52904039, 52907687, 52913767,
52915015, 52917607, 52935271, 52944743, 52945767, 52950247, 52958535, 52963431, 52964007,
52971335, 52974759, 52978407, 52981671, 52990791, 52993191, 53007591, 53016903, 53033319,
53039015, 53040999, 53057255, 53057639, 53059431, 53060455, 53061703, 53070183, 53085415,
53085799, 53100391, 53102663, 53113575, 53119847, 53128551, 53131591, 53137895, 53146983,
53148839, 53150439, 53155751, 53160007, 53162823, 53164647, 53179623, 53185895, 53190983,
53193639, 53195239, 53202151, 53216743, 53225639, 53235367, 53236391, 53263719, 53272423,
53273063, 53290855, 53291879, 53318471, 53331815, 53345383, 53346631, 53375815, 53385127,
53388135, 53395047, 53404391, 53407591, 53408615, 53417319, 53419367, 53425479, 53429735,
53438823, 53439207, 53442471, 53445479, 53447527, 53453639, 53461735, 53465959, 53472487,
53481799, 53486055, 53493927, 53506119, 53515431, 53517031, 53518663, 53537895, 53547847,
53548647, 53555367, 53556967, 53563463, 53563879, 53570375, 53571751, 53579495, 53584967,
53586151, 53591399, 53598311, 53602983, 53605607, 53626471, 53633767, 53636199, 53641287,
53654631, 53662375, 53662951, 53669031, 53678951, 53692135, 53697191, 53725351, 53726567,
53730023, 53735271, 53735911, 53738343, 53746855, 53755751, 53772615, 53785959, 53786791,
53792615, 53797959, 53807431, 53810279, 53813351, 53814119, 53829959, 53840711, 53841255,
53843111, 53844711, 53845351, 53850023, 53852007, 53854279, 53860967, 53874343, 53875943,
53885255, 53886055, 53902695, 53907175, 53925191, 53925991, 53931687, 53932103, 53947719,
53954375, 53957991, 53973831, 53976231, 53982951, 54000743, 54001991, 54016359, 54031175,
54034023, 54037671, 54057319, 54060359, 54061159, 54063591, 54074727, 54076775, 54093991,
54095015, 54098247, 54101863, 54104135, 54111591, 54114663, 54118503, 54141415, 54141799,
54151335, 54154983, 54159207, 54164327, 54170983, 54194919, 54212935, 54216807, 54220647,
54233191, 54242535, 54244167, 54245991, 54266023, 54274151, 54275399, 54276967, 54277991,
54288743, 54301927, 54310631, 54315943, 54324391, 54325415, 54330471, 54351175, 54354407,
54364519, 54367975, 54372263, 54384807, 54385383, 54391655, 54393703, 54396135, 54408295,
54409127, 54421863, 54424295, 54430567, 54431815, 54437479, 54445799, 54446183, 54455527,
54463591, 54466471, 54473959, 54476391, 54479015, 54480231, 54507367, 54509639, 54512295,
54523207, 54535783, 54540007, 54546279, 54562535, 54563143, 54596775, 54610759, 54616807,
54629607, 54637671, 54639719, 54643623, 54652263, 54657767, 54660967, 54670151, 54678855,
54699111, 54710439, 54715111, 54722631, 54733543, 54736199, 54738791, 54739815, 54753607,
54755431, 54756455, 54764359, 54765159, 54777703, 54779751, 54780391, 54792519, 54792935,
54795367, 54799207, 54807911, 54814023, 54817255, 54822119, 54823751, 54826343, 54832871,
54839783, 54842183, 54842983, 54855527, 54858599, 54858983, 54874599, 54880487, 54889191,
54897127, 54901351, 54902375, 54908231, 54909031, 54930759, 54931367, 54953447, 54960295,
54963367, 54965991, 54967399, 54973095, 54985031, 54985831, 54986855, 54989287, 54991527,
54996199, 54997831, 55022759, 55023335, 55025991, 55039335, 55051751, 55057575, 55057767,
55064487, 55067495, 55083335, 55083751, 55086951, 55098727, 55101767, 55102567, 55108071,
55114343, 55121831, 55124839, 55136423, 55146343, 55147175, 55148615, 55154023, 55156071,
55160743, 55161159, 55173287, 55175911, 55177959, 55185479, 55190343, 55201095, 55201639,
55205735, 55208007, 55227207, 55236327, 55242823, 55243239, 55248711, 55251111, 55257415,
55265351, 55281127, 55284967, 55298983, 55300583, 55311079, 55313127, 55318375, 55321671,
55323879, 55334215, 55334823, 55337447, 55341735, 55352039, 55357511, 55358311, 55363175,
55364423, 55365799, 55376743, 55391559, 55394407, 55398055, 55399079, 55417703, 55419975,
55433895, 55435111, 55451975, 55454375, 55465319, 55475047, 55476295, 55487207, 55487591,
55520615, 55524711, 55529383, 55529959, 55531367, 55544135, 55546183, 55565415, 55569319,
55578791, 55601319, 55602919, 55604551, 55609191, 55611463, 55624807, 55625639, 55628455,
55637351, 55638759, 55649351, 55653191, 55656039, 55662311, 55668807, 55679303, 55681351,
55692103, 55695527, 55705671, 55719015, 55720263, 55724903, 55725735, 55742951, 55745191,
55752295, 55754087, 55756519, 55763431, 55773351, 55778407, 55781223, 55782247, 55784295,
55784679, 55789799, 55790951, 55797863, 55815911, 55828647, 55834343, 55836775, 55838567,
55846119, 55848295, 55855431, 55857639, 55869607, 55872679, 55885415, 55896167, 55898183,
55914407, 55928999, 55932839, 55937511, 55945383, 55950439, 55956135, 55956327, 55971143,
55989991, 56006983, 56007399, 56030535, 56033767, 56037031, 56047527, 56059495, 56069991,
56093351, 56111175, 56111975, 56116839, 56124743, 56125543, 56131655, 56142951, 56150503,
56152903, 56153319, 56158023, 56162663, 56169319, 56182503, 56184135, 56186727, 56202567,
56203367, 56210663, 56214343, 56218983, 56219367, 56220007, 56225863, 56231527, 56236199,
56247143, 56262759, 56276327, 56277735, 56293991, 56296167, 56300263, 56305735, 56306919,
56319079, 56325351, 56331623, 56333479, 56339367, 56341351, 56351335, 56351911, 56356583,
56358215, 56371559, 56375623, 56389799, 56394087, 56394471, 56399719, 56401991, 56412903,
56413287, 56418151, 56419175, 56444135, 56448359, 56491111, 56507559, 56514407, 56514471,
56516455, 56518727, 56521543, 56533863, 56534119, 56534887, 56535719, 56538343, 56550727,
56552359, 56553959, 56563047, 56563879, 56566503, 56575463, 56578887, 56581735, 56584359,
56587591, 56595111, 56627943, 56631783, 56639655, 56645351, 56645959, 56646759, 56652455,
56664391, 56668487, 56670887, 56675143, 56684263, 56693575, 56696999, 56702119, 56718695,
56723559, 56724807, 56735335, 56737127, 56746855, 56758439, 56759463, 56762695, 56767335,
56772839, 56781127, 56781927, 56794279, 56797543, 56797927, 56804199, 56812359, 56814759,
56815783, 56824679, 56825703, 56835431, 56839271, 56854695, 56861543, 56875751, 56880999,
56906567, 56919911, 56922183, 56934727, 56943687, 56961703, 56966759
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.