New Syracuse step-14 certificate classes, chunk 3
DefinitionsyracuseSevenMod32New26Step14Chunk03Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 3 of 5 of the newly certifiable residue classes modulo with accelerated Syracuse descent time and total stripped exponent . This chunk contains 677 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 syracuseSevenMod32New26Step14Chunk03Classes : Finset ℕ := {
27343207, 27421415, 27427687, 27428711, 27469287, 27476135, 27501895, 27512039, 27530055,
27533479, 27535527, 27561287, 27564711, 27569383, 27592871, 27603015, 27634023, 27674951,
27679399, 27691367, 27707559, 27718503, 27747687, 27771623, 27789639, 27826343, 27835239,
27837511, 27863399, 27880263, 27915495, 27929511, 27937607, 27943655, 27971239, 28009319,
28055719, 28065639, 28114087, 28122983, 28139847, 28169831, 28207335, 28212583, 28238695,
28263655, 28283719, 28297063, 28311879, 28343911, 28384615, 28404903, 28406503, 28428391,
28461223, 28464295, 28521639, 28522215, 28575559, 28587879, 28620711, 28631879, 28684775,
28703591, 28747367, 28752039, 28754663, 28774727, 28775527, 28841191, 28872423, 28890439,
28892263, 28904807, 28925095, 28928743, 28929767, 28986087, 28994407, 29039783, 29051751,
29052999, 29064295, 29066343, 29122887, 29132007, 29142951, 29186727, 29195623, 29207015,
29209415, 29212839, 29222759, 29223783, 29240647, 29244071, 29253991, 29263335, 29272231,
29275879, 29296967, 29297991, 29313383, 29319655, 29354311, 29374375, 29421223, 29446311,
29500231, 29530215, 29542759, 29563623, 29575239, 29586535, 29594855, 29608871, 29610471,
29623015, 29624039, 29631559, 29644103, 29652199, 29666215, 29687879, 29701223, 29704295,
29708967, 29722535, 29744999, 29766887, 29791847, 29829351, 29854439, 29885671, 29913831,
29931847, 29951335, 29963079, 29966503, 29978695, 29991239, 29992263, 30020423, 30021223,
30058727, 30063975, 30073319, 30107751, 30112423, 30115047, 30135111, 30190055, 30197575,
30201575, 30222663, 30253895, 30265191, 30282055, 30317287, 30323559, 30346919, 30395495,
30403239, 30426727, 30426951, 30441543, 30483271, 30492391, 30520551, 30529895, 30547111,
30558279, 30569799, 30584167, 30586215, 30590887, 30593511, 30604455, 30650279, 30661223,
30673767, 30685511, 30692007, 30787431, 30811367, 30834855, 30860615, 30888775, 30894247,
30902119, 30903143, 30928103, 30955239, 30961735, 31012583, 31066279, 31069351, 31077223,
31125671, 31127271, 31149159, 31152231, 31179591, 31185063, 31208551, 31242407, 31242983,
31246055, 31265895, 31289831, 31296327, 31323463, 31329959, 31331559, 31380807, 31381607,
31409767, 31461863, 31472807, 31475431, 31495495, 31512935, 31533799, 31593191, 31597415,
31611207, 31614279, 31650535, 31658055, 31699783, 31744359, 31760551, 31763623, 31787111,
31791783, 31810023, 31830087, 31843655, 31880935, 31890279, 31902023, 31946599, 31961415,
31974759, 31979431, 31984103, 32002919, 32018759, 32034151, 32052391, 32134247, 32141991,
32171751, 32178247, 32193639, 32198311, 32249159, 32250983, 32263527, 32272871, 32287463,
32288487, 32329639, 32344807, 32352327, 32386983, 32409447, 32423015, 32425063, 32516839,
32539975, 32545447, 32550119, 32573607, 32602791, 32612711, 32641095, 32655687, 32656711,
32672103, 32691943, 32713031, 32733095, 32745639, 32756583, 32770151, 32774823, 32779495,
32813927, 32828519, 32873319, 32885063, 32918343, 32922343, 32928615, 32953575, 32979687,
33024935, 33060167, 33067687, 33081255, 33125607, 33147719, 33150567, 33152167, 33188071,
33198567, 33207911, 33213159, 33244391, 33245415, 33275751, 33290567, 33301735, 33306983,
33321799, 33325223, 33335143, 33347911, 33363303, 33381991, 33432039, 33438311, 33439911,
33471143, 33493831, 33502375, 33556295, 33566791, 33581383, 33612615, 33613639, 33658791,
33669959, 33676007, 33682279, 33733351, 33785447, 33790119, 33800263, 33813607, 33827175,
33872999, 33905831, 33907431, 33910503, 33949607, 33963175, 33966823, 33973095, 34029415,
34032487, 34044231, 34050727, 34101575, 34102375, 34116967, 34135207, 34139879, 34191975,
34196199, 34224807, 34252967, 34275655, 34278727, 34310311, 34313959, 34318183, 34335047,
34348391, 34412455, 34428071, 34454183, 34465127, 34469799, 34484391, 34485991, 34493287,
34508103, 34510951, 34564423, 34567271, 34568295, 34584487, 34601703, 34604775, 34624615,
34632935, 34646951, 34648551, 34662119, 34667367, 34682183, 34695527, 34703271, 34723687,
34742375, 34773159, 34796647, 34804967, 34811239, 34820583, 34831527, 34854215, 34876327,
34919079, 34932647, 34947239, 34956135, 34969927, 34972999, 35001159, 35009255, 35014503,
35016775, 35030343, 35103079, 35145831, 35173191, 35186535, 35187559, 35188807, 35283431,
35333479, 35338151, 35377479, 35384999, 35411111, 35412711, 35441319, 35464807, 35477351,
35490919, 35492967, 35506535, 35527399, 35585191, 35586791, 35628967, 35631591, 35651655,
35708775, 35745703, 35768167, 35780935, 35814567, 35824487, 35849447, 35872935, 35875559,
35881831, 35895623, 35908839, 35928679, 35955015, 35966183, 35971431, 35980775, 35984999,
35989671, 35993319, 35997543, 35999815, 36022503, 36027751, 36055911, 36115303, 36133543,
36149159, 36159079, 36161703, 36165351, 36171623, 36187239, 36217671, 36223143, 36243783,
36246631, 36277063, 36279463, 36281063, 36287335, 36312295, 36334407, 36348999, 36361543,
36368039, 36369639, 36390727, 36432231, 36476007, 36499943, 36533575, 36547943, 36631271,
36649287, 36680519, 36722023, 36725095, 36737863, 36750183, 36790759, 36801703, 36825191,
36832487, 36855975, 36860647, 36866919, 36868167, 36912743, 36954471, 36999495, 37148839,
37158983, 37170279, 37185895, 37200711, 37206759, 37209831, 37228871, 37231719, 37261479,
37266151, 37269223, 37325543, 37326567, 37345383, 37367719, 37463143, 37475687, 37493927,
37503847, 37519463, 37550695, 37552295, 37561191, 37574983, 37578055, 37583527, 37597095,
37634375, 37637447, 37650791, 37672679, 37693767, 37694791, 37707111, 37724327, 37730023,
37771175, 37792615, 37794663, 37823847, 37943207, 37966695, 38005671, 38015143, 38040903,
38048999, 38054247, 38061991, 38063015, 38082407, 38098247, 38105767, 38119335, 38131879,
38155367, 38162087, 38188647, 38192871, 38218407, 38221031, 38226151, 38227303, 38249191,
38251239, 38273127, 38282471, 38305959, 38371175, 38386791, 38401383, 38417223, 38470119,
38509223, 38527463, 38535335, 38546279, 38561095, 38589255, 38594375, 38617415, 38619463,
38649447, 38650695, 38690151, 38692199, 38701543, 38714087, 38743271, 38823527, 38836071,
38838343, 38849639, 38886119, 38895687, 38943911, 38972071, 39000231, 39067495, 39069767,
39082311, 39088807, 39095655, 39111495, 39152999, 39155047, 39183207, 39208167, 39212391,
39234279, 39254343, 39255143, 39291047, 39327079, 39339495, 39348391, 39356263, 39402087,
39409383, 39414631, 39445863, 39450535, 39466151, 39474023, 39492263, 39520423, 39531367,
39545959, 39549031, 39576391, 39578791, 39581415, 39602503, 39605351, 39622567, 39642855,
39675239, 39707719, 39733607, 39761767, 39777607, 39869607, 39930599, 39949639, 39989991,
40009831, 40011079, 40024423, 40047335, 40050535, 40066151, 40080743, 40083815, 40102631,
40103655, 40141159, 40183911, 40188583, 40191207, 40212071, 40240231, 40249575, 40271463,
40298823, 40332455
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.